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:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            a__incr#_A(x1) = ((1,0),(0,0)) x1 + (0,2)
            cons_A(x1,x2) = x1 + ((1,0),(1,0)) x2 + (0,3)
            mark#_A(x1) = ((1,0),(0,0)) x1 + (0,2)
            s_A(x1) = x1
            tail_A(x1) = x1 + (1,0)
            a__tail#_A(x1) = x1
            mark_A(x1) = x1
            head_A(x1) = x1 + (2,1)
            a__head#_A(x1) = x1 + (1,2)
            nats_A() = (3,8)
            a__nats#_A() = (3,2)
            a__adx#_A(x1) = ((1,0),(0,0)) x1 + (0,2)
            a__zeros_A() = (2,7)
            adx_A(x1) = ((1,0),(1,1)) x1
            incr_A(x1) = x1
            a__incr_A(x1) = x1
            nil_A() = (1,0)
            a__adx_A(x1) = ((1,0),(1,1)) x1
            a__nats_A() = (3,8)
            a__head_A(x1) = x1 + (2,1)
            a__tail_A(x1) = x1 + (1,0)
            |0|_A() = (0,1)
            zeros_A() = (2,7)
    
      precedence:
      
        mark = a__zeros = a__head = |0| > zeros > a__tail > s > a__adx > cons = adx = a__incr > tail > head = nats = a__nats > a__incr# = mark# = a__nats# = a__adx# = incr > a__tail# > a__head# = nil
      
      partial status:
    
        pi(a__incr#) = []
        pi(cons) = [1]
        pi(mark#) = []
        pi(s) = [1]
        pi(tail) = [1]
        pi(a__tail#) = [1]
        pi(mark) = [1]
        pi(head) = []
        pi(a__head#) = [1]
        pi(nats) = []
        pi(a__nats#) = []
        pi(a__adx#) = []
        pi(a__zeros) = []
        pi(adx) = [1]
        pi(incr) = [1]
        pi(a__incr) = [1]
        pi(nil) = []
        pi(a__adx) = [1]
        pi(a__nats) = []
        pi(a__head) = [1]
        pi(a__tail) = [1]
        pi(|0|) = []
        pi(zeros) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            a__incr#_A(x1) = (2,24)
            cons_A(x1,x2) = x1 + (9,10)
            mark#_A(x1) = (2,24)
            s_A(x1) = ((1,0),(0,0)) x1 + (3,16)
            tail_A(x1) = (1,12)
            a__tail#_A(x1) = (3,23)
            mark_A(x1) = ((0,0),(1,0)) x1 + (5,12)
            head_A(x1) = (3,0)
            a__head#_A(x1) = ((0,0),(1,0)) x1 + (2,19)
            nats_A() = (3,25)
            a__nats#_A() = (2,24)
            a__adx#_A(x1) = (2,24)
            a__zeros_A() = (11,11)
            adx_A(x1) = ((1,0),(0,0)) x1 + (19,23)
            incr_A(x1) = ((1,0),(0,0)) x1 + (1,9)
            a__incr_A(x1) = (18,10)
            nil_A() = (1,0)
            a__adx_A(x1) = (19,23)
            a__nats_A() = (4,14)
            a__head_A(x1) = (0,0)
            a__tail_A(x1) = ((0,0),(1,0)) x1 + (2,8)
            |0|_A() = (1,0)
            zeros_A() = (0,11)
    
      precedence:
      
        |0| > zeros > a__adx > nil > mark = head = a__head = a__tail > adx > s > a__zeros > cons = a__incr = a__nats > incr > a__incr# = mark# = a__tail# = a__head# = a__nats# = a__adx# > nats > tail
      
      partial status:
    
        pi(a__incr#) = []
        pi(cons) = []
        pi(mark#) = []
        pi(s) = []
        pi(tail) = []
        pi(a__tail#) = []
        pi(mark) = []
        pi(head) = []
        pi(a__head#) = []
        pi(nats) = []
        pi(a__nats#) = []
        pi(a__adx#) = []
        pi(a__zeros) = []
        pi(adx) = []
        pi(incr) = []
        pi(a__incr) = []
        pi(nil) = []
        pi(a__adx) = []
        pi(a__nats) = []
        pi(a__head) = []
        pi(a__tail) = []
        pi(|0|) = []
        pi(zeros) = []
    

The next rules are strictly ordered:

  p4, p5, p6

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: mark#(head(X)) -> mark#(X)
p5: mark#(head(X)) -> a__head#(mark(X))
p6: a__head#(cons(X,L)) -> mark#(X)
p7: mark#(nats()) -> a__nats#()
p8: a__nats#() -> a__adx#(a__zeros())
p9: a__adx#(cons(X,L)) -> mark#(X)
p10: mark#(adx(X)) -> mark#(X)
p11: mark#(adx(X)) -> a__adx#(mark(X))
p12: a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
p13: mark#(incr(X)) -> mark#(X)
p14: 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, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14}


-- 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: a__adx#(cons(X,L)) -> mark#(X)
p7: mark#(adx(X)) -> mark#(X)
p8: mark#(nats()) -> a__nats#()
p9: a__nats#() -> a__adx#(a__zeros())
p10: mark#(head(X)) -> a__head#(mark(X))
p11: a__head#(cons(X,L)) -> mark#(X)
p12: mark#(head(X)) -> mark#(X)
p13: mark#(cons(X1,X2)) -> mark#(X1)
p14: 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:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            a__incr#_A(x1) = x1 + (0,1)
            cons_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (0,2)
            mark#_A(x1) = ((1,0),(1,1)) x1
            incr_A(x1) = ((1,0),(1,1)) x1 + (0,3)
            mark_A(x1) = x1 + (0,2)
            adx_A(x1) = ((1,0),(1,1)) x1 + (1,7)
            a__adx#_A(x1) = x1 + (1,4)
            nats_A() = (4,12)
            a__nats#_A() = (3,13)
            a__zeros_A() = (1,4)
            head_A(x1) = ((1,0),(0,0)) x1 + (2,1)
            a__head#_A(x1) = ((1,0),(0,0)) x1 + (1,0)
            s_A(x1) = x1 + (0,1)
            a__incr_A(x1) = ((1,0),(1,1)) x1 + (0,3)
            nil_A() = (1,1)
            a__adx_A(x1) = ((1,0),(1,1)) x1 + (1,7)
            a__nats_A() = (4,13)
            a__head_A(x1) = ((1,0),(0,0)) x1 + (2,2)
            a__tail_A(x1) = ((1,0),(0,0)) x1 + (1,2)
            tail_A(x1) = ((1,0),(0,0)) x1 + (1,1)
            |0|_A() = (0,1)
            zeros_A() = (1,4)
    
      precedence:
      
        mark# = mark = a__nats# = a__head# = a__head = a__tail = |0| > a__adx# > a__adx > adx > head > a__zeros = a__nats > nats > a__incr > incr > a__incr# > cons > nil > s = tail = zeros
      
      partial status:
    
        pi(a__incr#) = [1]
        pi(cons) = [1]
        pi(mark#) = [1]
        pi(incr) = [1]
        pi(mark) = []
        pi(adx) = [1]
        pi(a__adx#) = [1]
        pi(nats) = []
        pi(a__nats#) = []
        pi(a__zeros) = []
        pi(head) = []
        pi(a__head#) = []
        pi(s) = [1]
        pi(a__incr) = [1]
        pi(nil) = []
        pi(a__adx) = [1]
        pi(a__nats) = []
        pi(a__head) = []
        pi(a__tail) = []
        pi(tail) = []
        pi(|0|) = []
        pi(zeros) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            a__incr#_A(x1) = x1 + (11,4)
            cons_A(x1,x2) = ((0,0),(1,0)) x1 + (1,4)
            mark#_A(x1) = ((0,0),(1,0)) x1 + (12,3)
            incr_A(x1) = ((1,0),(0,0)) x1 + (3,2)
            mark_A(x1) = (4,2)
            adx_A(x1) = ((1,0),(0,0)) x1 + (10,1)
            a__adx#_A(x1) = (12,13)
            nats_A() = (11,1)
            a__nats#_A() = (12,13)
            a__zeros_A() = (2,0)
            head_A(x1) = (3,1)
            a__head#_A(x1) = (13,6)
            s_A(x1) = ((1,0),(0,0)) x1 + (1,0)
            a__incr_A(x1) = (2,0)
            nil_A() = (3,2)
            a__adx_A(x1) = ((1,0),(0,0)) x1 + (11,2)
            a__nats_A() = (3,1)
            a__head_A(x1) = (4,2)
            a__tail_A(x1) = (4,2)
            tail_A(x1) = (3,2)
            |0|_A() = (5,3)
            zeros_A() = (0,1)
    
      precedence:
      
        |0| > zeros > tail > a__zeros > a__nats# > nats > a__incr# > mark# = a__adx# = a__head# > head > cons > mark = a__head = a__tail > a__nats > s > a__incr = nil = a__adx > adx > incr
      
      partial status:
    
        pi(a__incr#) = []
        pi(cons) = []
        pi(mark#) = []
        pi(incr) = []
        pi(mark) = []
        pi(adx) = []
        pi(a__adx#) = []
        pi(nats) = []
        pi(a__nats#) = []
        pi(a__zeros) = []
        pi(head) = []
        pi(a__head#) = []
        pi(s) = []
        pi(a__incr) = []
        pi(nil) = []
        pi(a__adx) = []
        pi(a__nats) = []
        pi(a__head) = []
        pi(a__tail) = []
        pi(tail) = []
        pi(|0|) = []
        pi(zeros) = []
    

The next rules are strictly ordered:

  p1, p2, p3, p6, p7, p10, p12, p13, p14

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(adx(X)) -> a__adx#(mark(X))
p2: a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
p3: mark#(nats()) -> a__nats#()
p4: a__nats#() -> a__adx#(a__zeros())
p5: a__head#(cons(X,L)) -> 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:

  (no SCCs)