YES

We show the termination of the TRS R:

  a__incr(nil()) -> nil()
  a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
  a__adx(nil()) -> nil()
  a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
  a__nats() -> a__adx(a__zeros())
  a__zeros() -> cons(|0|(),zeros())
  a__head(cons(X,L)) -> mark(X)
  a__tail(cons(X,L)) -> mark(L)
  mark(incr(X)) -> a__incr(mark(X))
  mark(adx(X)) -> a__adx(mark(X))
  mark(nats()) -> a__nats()
  mark(zeros()) -> a__zeros()
  mark(head(X)) -> a__head(mark(X))
  mark(tail(X)) -> a__tail(mark(X))
  mark(nil()) -> nil()
  mark(cons(X1,X2)) -> cons(mark(X1),X2)
  mark(s(X)) -> s(mark(X))
  mark(|0|()) -> |0|()
  a__incr(X) -> incr(X)
  a__adx(X) -> adx(X)
  a__nats() -> nats()
  a__zeros() -> zeros()
  a__head(X) -> head(X)
  a__tail(X) -> tail(X)

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: a__incr#(cons(X,L)) -> mark#(X)
p2: a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
p3: a__adx#(cons(X,L)) -> mark#(X)
p4: a__nats#() -> a__adx#(a__zeros())
p5: a__nats#() -> a__zeros#()
p6: a__head#(cons(X,L)) -> mark#(X)
p7: a__tail#(cons(X,L)) -> mark#(L)
p8: mark#(incr(X)) -> a__incr#(mark(X))
p9: mark#(incr(X)) -> mark#(X)
p10: mark#(adx(X)) -> a__adx#(mark(X))
p11: mark#(adx(X)) -> mark#(X)
p12: mark#(nats()) -> a__nats#()
p13: mark#(zeros()) -> a__zeros#()
p14: mark#(head(X)) -> a__head#(mark(X))
p15: mark#(head(X)) -> mark#(X)
p16: mark#(tail(X)) -> a__tail#(mark(X))
p17: mark#(tail(X)) -> mark#(X)
p18: mark#(cons(X1,X2)) -> mark#(X1)
p19: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__incr(nil()) -> nil()
r2: a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
r3: a__adx(nil()) -> nil()
r4: a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
r5: a__nats() -> a__adx(a__zeros())
r6: a__zeros() -> cons(|0|(),zeros())
r7: a__head(cons(X,L)) -> mark(X)
r8: a__tail(cons(X,L)) -> mark(L)
r9: mark(incr(X)) -> a__incr(mark(X))
r10: mark(adx(X)) -> a__adx(mark(X))
r11: mark(nats()) -> a__nats()
r12: mark(zeros()) -> a__zeros()
r13: mark(head(X)) -> a__head(mark(X))
r14: mark(tail(X)) -> a__tail(mark(X))
r15: mark(nil()) -> nil()
r16: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r17: mark(s(X)) -> s(mark(X))
r18: mark(|0|()) -> |0|()
r19: a__incr(X) -> incr(X)
r20: a__adx(X) -> adx(X)
r21: a__nats() -> nats()
r22: a__zeros() -> zeros()
r23: a__head(X) -> head(X)
r24: a__tail(X) -> tail(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p6, p7, p8, p9, p10, p11, p12, p14, p15, p16, p17, p18, p19}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: a__incr#(cons(X,L)) -> mark#(X)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(cons(X1,X2)) -> mark#(X1)
p4: mark#(tail(X)) -> mark#(X)
p5: mark#(tail(X)) -> a__tail#(mark(X))
p6: a__tail#(cons(X,L)) -> mark#(L)
p7: mark#(head(X)) -> mark#(X)
p8: mark#(head(X)) -> a__head#(mark(X))
p9: a__head#(cons(X,L)) -> mark#(X)
p10: mark#(nats()) -> a__nats#()
p11: a__nats#() -> a__adx#(a__zeros())
p12: a__adx#(cons(X,L)) -> mark#(X)
p13: mark#(adx(X)) -> mark#(X)
p14: mark#(adx(X)) -> a__adx#(mark(X))
p15: a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
p16: mark#(incr(X)) -> mark#(X)
p17: mark#(incr(X)) -> a__incr#(mark(X))

and R consists of:

r1: a__incr(nil()) -> nil()
r2: a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
r3: a__adx(nil()) -> nil()
r4: a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
r5: a__nats() -> a__adx(a__zeros())
r6: a__zeros() -> cons(|0|(),zeros())
r7: a__head(cons(X,L)) -> mark(X)
r8: a__tail(cons(X,L)) -> mark(L)
r9: mark(incr(X)) -> a__incr(mark(X))
r10: mark(adx(X)) -> a__adx(mark(X))
r11: mark(nats()) -> a__nats()
r12: mark(zeros()) -> a__zeros()
r13: mark(head(X)) -> a__head(mark(X))
r14: mark(tail(X)) -> a__tail(mark(X))
r15: mark(nil()) -> nil()
r16: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r17: mark(s(X)) -> s(mark(X))
r18: mark(|0|()) -> |0|()
r19: a__incr(X) -> incr(X)
r20: a__adx(X) -> adx(X)
r21: a__nats() -> nats()
r22: a__zeros() -> zeros()
r23: a__head(X) -> head(X)
r24: a__tail(X) -> tail(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      a__incr#_A(x1) = ((0,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x1
      cons_A(x1,x2) = ((1,0,0,0),(1,0,0,0),(0,1,0,0),(0,0,1,0)) x1 + ((1,0,0,0),(1,0,0,0),(0,1,0,0),(0,1,1,0)) x2 + (0,0,1,0)
      mark#_A(x1) = ((0,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x1
      s_A(x1) = x1 + (0,1,0,3)
      tail_A(x1) = ((1,0,0,0),(0,0,0,0),(0,0,0,0),(0,1,0,0)) x1 + (2,2,0,1)
      a__tail#_A(x1) = ((0,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x1 + (0,0,0,1)
      mark_A(x1) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(0,1,1,0)) x1 + (0,5,4,1)
      head_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,1,0,0)) x1 + (2,1,0,4)
      a__head#_A(x1) = ((0,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x1 + (0,0,0,1)
      nats_A() = (3,1,3,1)
      a__nats#_A() = (0,0,0,2)
      a__adx#_A(x1) = ((0,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x1 + (0,0,0,1)
      a__zeros_A() = (1,3,2,2)
      adx_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x1 + (1,2,5,1)
      incr_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(1,0,0,0)) x1 + (0,1,0,8)
      a__incr_A(x1) = ((1,0,0,0),(1,0,0,0),(1,0,0,0),(0,1,0,0)) x1 + (0,2,4,7)
      nil_A() = (0,1,4,9)
      a__adx_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x1 + (1,4,6,7)
      a__nats_A() = (3,4,7,6)
      a__head_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x1 + (2,6,4,3)
      a__tail_A(x1) = x1 + (2,5,5,0)
      |0|_A() = (0,0,0,2)
      zeros_A() = (1,2,1,1)

The next rules are strictly ordered:

  p4, p5, p6, p7, p8, p9, p10, p12, p13

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: a__incr#(cons(X,L)) -> mark#(X)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(cons(X1,X2)) -> mark#(X1)
p4: a__nats#() -> a__adx#(a__zeros())
p5: mark#(adx(X)) -> a__adx#(mark(X))
p6: a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
p7: mark#(incr(X)) -> mark#(X)
p8: mark#(incr(X)) -> a__incr#(mark(X))

and R consists of:

r1: a__incr(nil()) -> nil()
r2: a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
r3: a__adx(nil()) -> nil()
r4: a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
r5: a__nats() -> a__adx(a__zeros())
r6: a__zeros() -> cons(|0|(),zeros())
r7: a__head(cons(X,L)) -> mark(X)
r8: a__tail(cons(X,L)) -> mark(L)
r9: mark(incr(X)) -> a__incr(mark(X))
r10: mark(adx(X)) -> a__adx(mark(X))
r11: mark(nats()) -> a__nats()
r12: mark(zeros()) -> a__zeros()
r13: mark(head(X)) -> a__head(mark(X))
r14: mark(tail(X)) -> a__tail(mark(X))
r15: mark(nil()) -> nil()
r16: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r17: mark(s(X)) -> s(mark(X))
r18: mark(|0|()) -> |0|()
r19: a__incr(X) -> incr(X)
r20: a__adx(X) -> adx(X)
r21: a__nats() -> nats()
r22: a__zeros() -> zeros()
r23: a__head(X) -> head(X)
r24: a__tail(X) -> tail(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p5, p6, p7, p8}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: a__incr#(cons(X,L)) -> mark#(X)
p2: mark#(incr(X)) -> a__incr#(mark(X))
p3: mark#(incr(X)) -> mark#(X)
p4: mark#(adx(X)) -> a__adx#(mark(X))
p5: a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
p6: mark#(cons(X1,X2)) -> mark#(X1)
p7: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__incr(nil()) -> nil()
r2: a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
r3: a__adx(nil()) -> nil()
r4: a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
r5: a__nats() -> a__adx(a__zeros())
r6: a__zeros() -> cons(|0|(),zeros())
r7: a__head(cons(X,L)) -> mark(X)
r8: a__tail(cons(X,L)) -> mark(L)
r9: mark(incr(X)) -> a__incr(mark(X))
r10: mark(adx(X)) -> a__adx(mark(X))
r11: mark(nats()) -> a__nats()
r12: mark(zeros()) -> a__zeros()
r13: mark(head(X)) -> a__head(mark(X))
r14: mark(tail(X)) -> a__tail(mark(X))
r15: mark(nil()) -> nil()
r16: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r17: mark(s(X)) -> s(mark(X))
r18: mark(|0|()) -> |0|()
r19: a__incr(X) -> incr(X)
r20: a__adx(X) -> adx(X)
r21: a__nats() -> nats()
r22: a__zeros() -> zeros()
r23: a__head(X) -> head(X)
r24: a__tail(X) -> tail(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      a__incr#_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,0,0),(0,1,1,0)) x1 + (0,0,6,0)
      cons_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,0,1,0),(0,1,0,0)) x1 + x2 + (0,4,7,2)
      mark#_A(x1) = ((1,0,0,0),(1,1,0,0),(0,0,1,0),(0,0,1,1)) x1 + (0,1,4,12)
      incr_A(x1) = ((1,0,0,0),(0,1,0,0),(1,1,1,0),(0,0,0,0)) x1 + (0,0,1,1)
      mark_A(x1) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(1,0,0,0)) x1 + (0,0,3,2)
      adx_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,0,0,1)) x1 + (1,6,0,1)
      a__adx#_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(1,1,1,1)) x1 + (1,7,0,9)
      s_A(x1) = x1 + (0,0,1,1)
      a__incr_A(x1) = ((1,0,0,0),(0,1,0,0),(1,1,1,0),(0,0,0,0)) x1 + (0,0,1,2)
      nil_A() = (0,0,0,5)
      a__adx_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(0,0,0,0)) x1 + (1,6,5,4)
      a__nats_A() = (1,12,20,5)
      a__zeros_A() = (0,6,9,4)
      |0|_A() = (0,1,1,1)
      zeros_A() = (0,6,9,4)
      a__head_A(x1) = x1 + (1,1,2,4)
      a__tail_A(x1) = x1 + (1,1,2,1)
      nats_A() = (1,12,6,0)
      head_A(x1) = x1 + (1,1,1,5)
      tail_A(x1) = ((1,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x1 + (1,1,1,0)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7

We remove them from the problem.  Then no dependency pair remains.