YES

We show the termination of the TRS R:

  a__U11(tt(),V2) -> a__U12(a__isNat(V2))
  a__U12(tt()) -> tt()
  a__U21(tt()) -> tt()
  a__U31(tt(),N) -> mark(N)
  a__U41(tt(),M,N) -> a__U42(a__isNat(N),M,N)
  a__U42(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
  a__isNat(|0|()) -> tt()
  a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
  a__isNat(s(V1)) -> a__U21(a__isNat(V1))
  a__plus(N,|0|()) -> a__U31(a__isNat(N),N)
  a__plus(N,s(M)) -> a__U41(a__isNat(M),M,N)
  mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
  mark(U12(X)) -> a__U12(mark(X))
  mark(isNat(X)) -> a__isNat(X)
  mark(U21(X)) -> a__U21(mark(X))
  mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
  mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
  mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
  mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
  mark(tt()) -> tt()
  mark(s(X)) -> s(mark(X))
  mark(|0|()) -> |0|()
  a__U11(X1,X2) -> U11(X1,X2)
  a__U12(X) -> U12(X)
  a__isNat(X) -> isNat(X)
  a__U21(X) -> U21(X)
  a__U31(X1,X2) -> U31(X1,X2)
  a__U41(X1,X2,X3) -> U41(X1,X2,X3)
  a__U42(X1,X2,X3) -> U42(X1,X2,X3)
  a__plus(X1,X2) -> plus(X1,X2)

-- SCC decomposition.

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

p1: a__U11#(tt(),V2) -> a__U12#(a__isNat(V2))
p2: a__U11#(tt(),V2) -> a__isNat#(V2)
p3: a__U31#(tt(),N) -> mark#(N)
p4: a__U41#(tt(),M,N) -> a__U42#(a__isNat(N),M,N)
p5: a__U41#(tt(),M,N) -> a__isNat#(N)
p6: a__U42#(tt(),M,N) -> a__plus#(mark(N),mark(M))
p7: a__U42#(tt(),M,N) -> mark#(N)
p8: a__U42#(tt(),M,N) -> mark#(M)
p9: a__isNat#(plus(V1,V2)) -> a__U11#(a__isNat(V1),V2)
p10: a__isNat#(plus(V1,V2)) -> a__isNat#(V1)
p11: a__isNat#(s(V1)) -> a__U21#(a__isNat(V1))
p12: a__isNat#(s(V1)) -> a__isNat#(V1)
p13: a__plus#(N,|0|()) -> a__U31#(a__isNat(N),N)
p14: a__plus#(N,|0|()) -> a__isNat#(N)
p15: a__plus#(N,s(M)) -> a__U41#(a__isNat(M),M,N)
p16: a__plus#(N,s(M)) -> a__isNat#(M)
p17: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2)
p18: mark#(U11(X1,X2)) -> mark#(X1)
p19: mark#(U12(X)) -> a__U12#(mark(X))
p20: mark#(U12(X)) -> mark#(X)
p21: mark#(isNat(X)) -> a__isNat#(X)
p22: mark#(U21(X)) -> a__U21#(mark(X))
p23: mark#(U21(X)) -> mark#(X)
p24: mark#(U31(X1,X2)) -> a__U31#(mark(X1),X2)
p25: mark#(U31(X1,X2)) -> mark#(X1)
p26: mark#(U41(X1,X2,X3)) -> a__U41#(mark(X1),X2,X3)
p27: mark#(U41(X1,X2,X3)) -> mark#(X1)
p28: mark#(U42(X1,X2,X3)) -> a__U42#(mark(X1),X2,X3)
p29: mark#(U42(X1,X2,X3)) -> mark#(X1)
p30: mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
p31: mark#(plus(X1,X2)) -> mark#(X1)
p32: mark#(plus(X1,X2)) -> mark#(X2)
p33: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__U11(tt(),V2) -> a__U12(a__isNat(V2))
r2: a__U12(tt()) -> tt()
r3: a__U21(tt()) -> tt()
r4: a__U31(tt(),N) -> mark(N)
r5: a__U41(tt(),M,N) -> a__U42(a__isNat(N),M,N)
r6: a__U42(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r7: a__isNat(|0|()) -> tt()
r8: a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
r9: a__isNat(s(V1)) -> a__U21(a__isNat(V1))
r10: a__plus(N,|0|()) -> a__U31(a__isNat(N),N)
r11: a__plus(N,s(M)) -> a__U41(a__isNat(M),M,N)
r12: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r13: mark(U12(X)) -> a__U12(mark(X))
r14: mark(isNat(X)) -> a__isNat(X)
r15: mark(U21(X)) -> a__U21(mark(X))
r16: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r17: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r18: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r19: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r20: mark(tt()) -> tt()
r21: mark(s(X)) -> s(mark(X))
r22: mark(|0|()) -> |0|()
r23: a__U11(X1,X2) -> U11(X1,X2)
r24: a__U12(X) -> U12(X)
r25: a__isNat(X) -> isNat(X)
r26: a__U21(X) -> U21(X)
r27: a__U31(X1,X2) -> U31(X1,X2)
r28: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r29: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r30: a__plus(X1,X2) -> plus(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p3, p4, p6, p7, p8, p13, p15, p18, p20, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32, p33}
  {p2, p9, p10, p12}


-- Reduction pair.

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

p1: a__U42#(tt(),M,N) -> mark#(M)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(plus(X1,X2)) -> mark#(X2)
p4: mark#(plus(X1,X2)) -> mark#(X1)
p5: mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
p6: a__plus#(N,s(M)) -> a__U41#(a__isNat(M),M,N)
p7: a__U41#(tt(),M,N) -> a__U42#(a__isNat(N),M,N)
p8: a__U42#(tt(),M,N) -> mark#(N)
p9: mark#(U42(X1,X2,X3)) -> mark#(X1)
p10: mark#(U42(X1,X2,X3)) -> a__U42#(mark(X1),X2,X3)
p11: a__U42#(tt(),M,N) -> a__plus#(mark(N),mark(M))
p12: a__plus#(N,|0|()) -> a__U31#(a__isNat(N),N)
p13: a__U31#(tt(),N) -> mark#(N)
p14: mark#(U41(X1,X2,X3)) -> mark#(X1)
p15: mark#(U41(X1,X2,X3)) -> a__U41#(mark(X1),X2,X3)
p16: mark#(U31(X1,X2)) -> mark#(X1)
p17: mark#(U31(X1,X2)) -> a__U31#(mark(X1),X2)
p18: mark#(U21(X)) -> mark#(X)
p19: mark#(U12(X)) -> mark#(X)
p20: mark#(U11(X1,X2)) -> mark#(X1)

and R consists of:

r1: a__U11(tt(),V2) -> a__U12(a__isNat(V2))
r2: a__U12(tt()) -> tt()
r3: a__U21(tt()) -> tt()
r4: a__U31(tt(),N) -> mark(N)
r5: a__U41(tt(),M,N) -> a__U42(a__isNat(N),M,N)
r6: a__U42(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r7: a__isNat(|0|()) -> tt()
r8: a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
r9: a__isNat(s(V1)) -> a__U21(a__isNat(V1))
r10: a__plus(N,|0|()) -> a__U31(a__isNat(N),N)
r11: a__plus(N,s(M)) -> a__U41(a__isNat(M),M,N)
r12: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r13: mark(U12(X)) -> a__U12(mark(X))
r14: mark(isNat(X)) -> a__isNat(X)
r15: mark(U21(X)) -> a__U21(mark(X))
r16: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r17: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r18: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r19: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r20: mark(tt()) -> tt()
r21: mark(s(X)) -> s(mark(X))
r22: mark(|0|()) -> |0|()
r23: a__U11(X1,X2) -> U11(X1,X2)
r24: a__U12(X) -> U12(X)
r25: a__isNat(X) -> isNat(X)
r26: a__U21(X) -> U21(X)
r27: a__U31(X1,X2) -> U31(X1,X2)
r28: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r29: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r30: a__plus(X1,X2) -> plus(X1,X2)

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, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__U42#_A(x1,x2,x3) = max{x1 - 6, x2 + 11, x3 + 10}
          tt_A = 45
          mark#_A(x1) = max{9, x1 + 2}
          s_A(x1) = max{8, x1}
          plus_A(x1,x2) = max{94, x1 + 79, x2 + 64}
          a__plus#_A(x1,x2) = max{x1 + 10, x2 + 11}
          mark_A(x1) = max{14, x1}
          a__U41#_A(x1,x2,x3) = max{x1 - 2, x2 + 11, x3 + 10}
          a__isNat_A(x1) = max{7, x1}
          U42_A(x1,x2,x3) = max{x1 + 49, x2 + 64, x3 + 79}
          |0|_A = 46
          a__U31#_A(x1,x2) = max{x1 + 1, x2 + 10}
          U41_A(x1,x2,x3) = max{x1 + 11, x2 + 64, x3 + 79}
          U31_A(x1,x2) = max{x1 + 2, x2 + 18}
          U21_A(x1) = max{8, x1}
          U12_A(x1) = max{55, x1 + 41}
          U11_A(x1,x2) = max{x1 + 2, x2 + 56}
          a__U11_A(x1,x2) = max{x1 + 2, x2 + 56}
          a__U12_A(x1) = max{55, x1 + 41}
          a__U21_A(x1) = max{8, x1}
          a__U31_A(x1,x2) = max{x1 + 2, x2 + 18}
          a__U41_A(x1,x2,x3) = max{x1 + 11, x2 + 64, x3 + 79}
          a__U42_A(x1,x2,x3) = max{x1 + 49, x2 + 64, x3 + 79}
          a__plus_A(x1,x2) = max{94, x1 + 79, x2 + 64}
          isNat_A(x1) = x1
    
      precedence:
      
        s = mark = a__isNat = U21 = a__U21 = a__U41 = a__U42 = a__plus > a__U11 > U11 > U42 > tt = a__U31 = isNat > U31 > a__U42# = a__plus# = a__U41# = U41 > |0| > mark# = plus = a__U31# = U12 = a__U12
      
      partial status:
    
        pi(a__U42#) = []
        pi(tt) = []
        pi(mark#) = [1]
        pi(s) = []
        pi(plus) = []
        pi(a__plus#) = []
        pi(mark) = []
        pi(a__U41#) = []
        pi(a__isNat) = []
        pi(U42) = []
        pi(|0|) = []
        pi(a__U31#) = []
        pi(U41) = []
        pi(U31) = []
        pi(U21) = []
        pi(U12) = []
        pi(U11) = [1]
        pi(a__U11) = [1, 2]
        pi(a__U12) = [1]
        pi(a__U21) = []
        pi(a__U31) = []
        pi(a__U41) = []
        pi(a__U42) = []
        pi(a__plus) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__U42#_A(x1,x2,x3) = 50
          tt_A = 0
          mark#_A(x1) = 50
          s_A(x1) = 18
          plus_A(x1,x2) = 9
          a__plus#_A(x1,x2) = 50
          mark_A(x1) = 32
          a__U41#_A(x1,x2,x3) = 50
          a__isNat_A(x1) = 20
          U42_A(x1,x2,x3) = 13
          |0|_A = 33
          a__U31#_A(x1,x2) = 50
          U41_A(x1,x2,x3) = 30
          U31_A(x1,x2) = 31
          U21_A(x1) = 1
          U12_A(x1) = 1
          U11_A(x1,x2) = max{49, x1 - 7}
          a__U11_A(x1,x2) = max{50, x1 - 7, x2 + 48}
          a__U12_A(x1) = 31
          a__U21_A(x1) = 19
          a__U31_A(x1,x2) = 32
          a__U41_A(x1,x2,x3) = 31
          a__U42_A(x1,x2,x3) = 30
          a__plus_A(x1,x2) = 32
          isNat_A(x1) = 19
    
      precedence:
      
        a__U42# = mark# = a__plus# = a__U41# = a__U31# > U21 > mark = a__U12 = a__plus > a__U31 > a__isNat > tt = s > a__U41 > plus > |0| = U41 = isNat > U11 = a__U11 > a__U42 > U12 > U42 = U31 = a__U21
      
      partial status:
    
        pi(a__U42#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(s) = []
        pi(plus) = []
        pi(a__plus#) = []
        pi(mark) = []
        pi(a__U41#) = []
        pi(a__isNat) = []
        pi(U42) = []
        pi(|0|) = []
        pi(a__U31#) = []
        pi(U41) = []
        pi(U31) = []
        pi(U21) = []
        pi(U12) = []
        pi(U11) = []
        pi(a__U11) = [2]
        pi(a__U12) = []
        pi(a__U21) = []
        pi(a__U31) = []
        pi(a__U41) = []
        pi(a__U42) = []
        pi(a__plus) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p15

We remove them from the problem.

-- SCC decomposition.

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

p1: a__U42#(tt(),M,N) -> mark#(M)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(plus(X1,X2)) -> mark#(X2)
p4: mark#(plus(X1,X2)) -> mark#(X1)
p5: mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
p6: a__plus#(N,s(M)) -> a__U41#(a__isNat(M),M,N)
p7: a__U41#(tt(),M,N) -> a__U42#(a__isNat(N),M,N)
p8: a__U42#(tt(),M,N) -> mark#(N)
p9: mark#(U42(X1,X2,X3)) -> mark#(X1)
p10: mark#(U42(X1,X2,X3)) -> a__U42#(mark(X1),X2,X3)
p11: a__U42#(tt(),M,N) -> a__plus#(mark(N),mark(M))
p12: a__plus#(N,|0|()) -> a__U31#(a__isNat(N),N)
p13: a__U31#(tt(),N) -> mark#(N)
p14: mark#(U41(X1,X2,X3)) -> mark#(X1)
p15: mark#(U31(X1,X2)) -> mark#(X1)
p16: mark#(U31(X1,X2)) -> a__U31#(mark(X1),X2)
p17: mark#(U21(X)) -> mark#(X)
p18: mark#(U12(X)) -> mark#(X)
p19: mark#(U11(X1,X2)) -> mark#(X1)

and R consists of:

r1: a__U11(tt(),V2) -> a__U12(a__isNat(V2))
r2: a__U12(tt()) -> tt()
r3: a__U21(tt()) -> tt()
r4: a__U31(tt(),N) -> mark(N)
r5: a__U41(tt(),M,N) -> a__U42(a__isNat(N),M,N)
r6: a__U42(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r7: a__isNat(|0|()) -> tt()
r8: a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
r9: a__isNat(s(V1)) -> a__U21(a__isNat(V1))
r10: a__plus(N,|0|()) -> a__U31(a__isNat(N),N)
r11: a__plus(N,s(M)) -> a__U41(a__isNat(M),M,N)
r12: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r13: mark(U12(X)) -> a__U12(mark(X))
r14: mark(isNat(X)) -> a__isNat(X)
r15: mark(U21(X)) -> a__U21(mark(X))
r16: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r17: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r18: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r19: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r20: mark(tt()) -> tt()
r21: mark(s(X)) -> s(mark(X))
r22: mark(|0|()) -> |0|()
r23: a__U11(X1,X2) -> U11(X1,X2)
r24: a__U12(X) -> U12(X)
r25: a__isNat(X) -> isNat(X)
r26: a__U21(X) -> U21(X)
r27: a__U31(X1,X2) -> U31(X1,X2)
r28: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r29: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r30: a__plus(X1,X2) -> plus(X1,X2)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: a__U42#(tt(),M,N) -> mark#(M)
p2: mark#(U11(X1,X2)) -> mark#(X1)
p3: mark#(U12(X)) -> mark#(X)
p4: mark#(U21(X)) -> mark#(X)
p5: mark#(U31(X1,X2)) -> a__U31#(mark(X1),X2)
p6: a__U31#(tt(),N) -> mark#(N)
p7: mark#(U31(X1,X2)) -> mark#(X1)
p8: mark#(U41(X1,X2,X3)) -> mark#(X1)
p9: mark#(U42(X1,X2,X3)) -> a__U42#(mark(X1),X2,X3)
p10: a__U42#(tt(),M,N) -> a__plus#(mark(N),mark(M))
p11: a__plus#(N,|0|()) -> a__U31#(a__isNat(N),N)
p12: a__plus#(N,s(M)) -> a__U41#(a__isNat(M),M,N)
p13: a__U41#(tt(),M,N) -> a__U42#(a__isNat(N),M,N)
p14: a__U42#(tt(),M,N) -> mark#(N)
p15: mark#(U42(X1,X2,X3)) -> mark#(X1)
p16: mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
p17: mark#(plus(X1,X2)) -> mark#(X1)
p18: mark#(plus(X1,X2)) -> mark#(X2)
p19: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__U11(tt(),V2) -> a__U12(a__isNat(V2))
r2: a__U12(tt()) -> tt()
r3: a__U21(tt()) -> tt()
r4: a__U31(tt(),N) -> mark(N)
r5: a__U41(tt(),M,N) -> a__U42(a__isNat(N),M,N)
r6: a__U42(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r7: a__isNat(|0|()) -> tt()
r8: a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
r9: a__isNat(s(V1)) -> a__U21(a__isNat(V1))
r10: a__plus(N,|0|()) -> a__U31(a__isNat(N),N)
r11: a__plus(N,s(M)) -> a__U41(a__isNat(M),M,N)
r12: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r13: mark(U12(X)) -> a__U12(mark(X))
r14: mark(isNat(X)) -> a__isNat(X)
r15: mark(U21(X)) -> a__U21(mark(X))
r16: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r17: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r18: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r19: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r20: mark(tt()) -> tt()
r21: mark(s(X)) -> s(mark(X))
r22: mark(|0|()) -> |0|()
r23: a__U11(X1,X2) -> U11(X1,X2)
r24: a__U12(X) -> U12(X)
r25: a__isNat(X) -> isNat(X)
r26: a__U21(X) -> U21(X)
r27: a__U31(X1,X2) -> U31(X1,X2)
r28: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r29: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r30: a__plus(X1,X2) -> plus(X1,X2)

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, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__U42#_A(x1,x2,x3) = max{x1 + 20, x2 + 15, x3 + 14}
          tt_A = 0
          mark#_A(x1) = max{9, x1 - 7}
          U11_A(x1,x2) = max{x1 + 15, x2 + 21}
          U12_A(x1) = max{16, x1 + 10}
          U21_A(x1) = max{17, x1}
          U31_A(x1,x2) = max{x1 + 23, x2 + 29}
          a__U31#_A(x1,x2) = max{x1 + 10, x2 + 10}
          mark_A(x1) = max{5, x1}
          U41_A(x1,x2,x3) = max{70, x1, x2 + 37, x3 + 37}
          U42_A(x1,x2,x3) = max{44, x1 + 33, x2 + 37, x3 + 37}
          a__plus#_A(x1,x2) = max{x1 + 14, x2 + 15}
          |0|_A = 10
          a__isNat_A(x1) = max{3, x1 - 9}
          s_A(x1) = max{33, x1}
          a__U41#_A(x1,x2,x3) = max{x1 + 23, x2 + 15, x3 + 14}
          plus_A(x1,x2) = max{43, x1 + 37, x2 + 37}
          a__U11_A(x1,x2) = max{x1 + 15, x2 + 21}
          a__U12_A(x1) = max{16, x1 + 10}
          a__U21_A(x1) = max{17, x1}
          a__U31_A(x1,x2) = max{x1 + 23, x2 + 29}
          a__U41_A(x1,x2,x3) = max{70, x1, x2 + 37, x3 + 37}
          a__U42_A(x1,x2,x3) = max{44, x1 + 33, x2 + 37, x3 + 37}
          a__plus_A(x1,x2) = max{43, x1 + 37, x2 + 37}
          isNat_A(x1) = max{3, x1 - 9}
    
      precedence:
      
        mark > a__plus > tt = a__isNat = plus = a__U11 > a__U42# = mark# = U11 = U12 = U21 = U31 = a__U31# = U41 = U42 = a__plus# = |0| = s = a__U41# = a__U12 = a__U21 = a__U31 = a__U41 = a__U42 = isNat
      
      partial status:
    
        pi(a__U42#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(U11) = []
        pi(U12) = []
        pi(U21) = []
        pi(U31) = []
        pi(a__U31#) = [2]
        pi(mark) = []
        pi(U41) = []
        pi(U42) = []
        pi(a__plus#) = []
        pi(|0|) = []
        pi(a__isNat) = []
        pi(s) = []
        pi(a__U41#) = []
        pi(plus) = [1, 2]
        pi(a__U11) = [1, 2]
        pi(a__U12) = []
        pi(a__U21) = []
        pi(a__U31) = []
        pi(a__U41) = []
        pi(a__U42) = []
        pi(a__plus) = [2]
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__U42#_A(x1,x2,x3) = 2
          tt_A = 65
          mark#_A(x1) = 2
          U11_A(x1,x2) = 106
          U12_A(x1) = 1
          U21_A(x1) = 62
          U31_A(x1,x2) = 159
          a__U31#_A(x1,x2) = x2 + 86
          mark_A(x1) = 160
          U41_A(x1,x2,x3) = 62
          U42_A(x1,x2,x3) = 59
          a__plus#_A(x1,x2) = 2
          |0|_A = 66
          a__isNat_A(x1) = 64
          s_A(x1) = 1
          a__U41#_A(x1,x2,x3) = 2
          plus_A(x1,x2) = max{63, x1 + 10, x2 + 15}
          a__U11_A(x1,x2) = max{16, x2 + 14}
          a__U12_A(x1) = 13
          a__U21_A(x1) = 63
          a__U31_A(x1,x2) = 160
          a__U41_A(x1,x2,x3) = 62
          a__U42_A(x1,x2,x3) = 60
          a__plus_A(x1,x2) = 63
          isNat_A(x1) = 82
    
      precedence:
      
        isNat > U21 > U11 > a__U21 > mark > |0| > a__U11 > a__U41 > a__U42 > U42 > plus > a__U42# = mark# = a__plus# = a__U41# > a__isNat > a__plus > tt > U41 > s > a__U31 > a__U31# > a__U12 > U31 > U12
      
      partial status:
    
        pi(a__U42#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(U11) = []
        pi(U12) = []
        pi(U21) = []
        pi(U31) = []
        pi(a__U31#) = []
        pi(mark) = []
        pi(U41) = []
        pi(U42) = []
        pi(a__plus#) = []
        pi(|0|) = []
        pi(a__isNat) = []
        pi(s) = []
        pi(a__U41#) = []
        pi(plus) = [2]
        pi(a__U11) = [2]
        pi(a__U12) = []
        pi(a__U21) = []
        pi(a__U31) = []
        pi(a__U41) = []
        pi(a__U42) = []
        pi(a__plus) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p1, p5, p6, p11, p15

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(U11(X1,X2)) -> mark#(X1)
p2: mark#(U12(X)) -> mark#(X)
p3: mark#(U21(X)) -> mark#(X)
p4: mark#(U31(X1,X2)) -> mark#(X1)
p5: mark#(U41(X1,X2,X3)) -> mark#(X1)
p6: mark#(U42(X1,X2,X3)) -> a__U42#(mark(X1),X2,X3)
p7: a__U42#(tt(),M,N) -> a__plus#(mark(N),mark(M))
p8: a__plus#(N,s(M)) -> a__U41#(a__isNat(M),M,N)
p9: a__U41#(tt(),M,N) -> a__U42#(a__isNat(N),M,N)
p10: a__U42#(tt(),M,N) -> mark#(N)
p11: mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
p12: mark#(plus(X1,X2)) -> mark#(X1)
p13: mark#(plus(X1,X2)) -> mark#(X2)
p14: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__U11(tt(),V2) -> a__U12(a__isNat(V2))
r2: a__U12(tt()) -> tt()
r3: a__U21(tt()) -> tt()
r4: a__U31(tt(),N) -> mark(N)
r5: a__U41(tt(),M,N) -> a__U42(a__isNat(N),M,N)
r6: a__U42(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r7: a__isNat(|0|()) -> tt()
r8: a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
r9: a__isNat(s(V1)) -> a__U21(a__isNat(V1))
r10: a__plus(N,|0|()) -> a__U31(a__isNat(N),N)
r11: a__plus(N,s(M)) -> a__U41(a__isNat(M),M,N)
r12: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r13: mark(U12(X)) -> a__U12(mark(X))
r14: mark(isNat(X)) -> a__isNat(X)
r15: mark(U21(X)) -> a__U21(mark(X))
r16: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r17: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r18: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r19: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r20: mark(tt()) -> tt()
r21: mark(s(X)) -> s(mark(X))
r22: mark(|0|()) -> |0|()
r23: a__U11(X1,X2) -> U11(X1,X2)
r24: a__U12(X) -> U12(X)
r25: a__isNat(X) -> isNat(X)
r26: a__U21(X) -> U21(X)
r27: a__U31(X1,X2) -> U31(X1,X2)
r28: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r29: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r30: a__plus(X1,X2) -> plus(X1,X2)

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: mark#(U11(X1,X2)) -> mark#(X1)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(plus(X1,X2)) -> mark#(X2)
p4: mark#(plus(X1,X2)) -> mark#(X1)
p5: mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
p6: a__plus#(N,s(M)) -> a__U41#(a__isNat(M),M,N)
p7: a__U41#(tt(),M,N) -> a__U42#(a__isNat(N),M,N)
p8: a__U42#(tt(),M,N) -> mark#(N)
p9: mark#(U42(X1,X2,X3)) -> a__U42#(mark(X1),X2,X3)
p10: a__U42#(tt(),M,N) -> a__plus#(mark(N),mark(M))
p11: mark#(U41(X1,X2,X3)) -> mark#(X1)
p12: mark#(U31(X1,X2)) -> mark#(X1)
p13: mark#(U21(X)) -> mark#(X)
p14: mark#(U12(X)) -> mark#(X)

and R consists of:

r1: a__U11(tt(),V2) -> a__U12(a__isNat(V2))
r2: a__U12(tt()) -> tt()
r3: a__U21(tt()) -> tt()
r4: a__U31(tt(),N) -> mark(N)
r5: a__U41(tt(),M,N) -> a__U42(a__isNat(N),M,N)
r6: a__U42(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r7: a__isNat(|0|()) -> tt()
r8: a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
r9: a__isNat(s(V1)) -> a__U21(a__isNat(V1))
r10: a__plus(N,|0|()) -> a__U31(a__isNat(N),N)
r11: a__plus(N,s(M)) -> a__U41(a__isNat(M),M,N)
r12: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r13: mark(U12(X)) -> a__U12(mark(X))
r14: mark(isNat(X)) -> a__isNat(X)
r15: mark(U21(X)) -> a__U21(mark(X))
r16: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r17: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r18: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r19: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r20: mark(tt()) -> tt()
r21: mark(s(X)) -> s(mark(X))
r22: mark(|0|()) -> |0|()
r23: a__U11(X1,X2) -> U11(X1,X2)
r24: a__U12(X) -> U12(X)
r25: a__isNat(X) -> isNat(X)
r26: a__U21(X) -> U21(X)
r27: a__U31(X1,X2) -> U31(X1,X2)
r28: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r29: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r30: a__plus(X1,X2) -> plus(X1,X2)

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, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{9, x1 + 5}
          U11_A(x1,x2) = max{x1 + 11, x2 + 31}
          s_A(x1) = x1
          plus_A(x1,x2) = max{x1 + 12, x2 + 34}
          a__plus#_A(x1,x2) = max{9, x1 + 6, x2 + 7}
          mark_A(x1) = x1
          a__U41#_A(x1,x2,x3) = max{9, x2 + 7, x3 + 6}
          a__isNat_A(x1) = max{13, x1 - 2}
          tt_A = 13
          a__U42#_A(x1,x2,x3) = max{x1 - 4, x2 + 7, x3 + 6}
          U42_A(x1,x2,x3) = max{x1 - 3, x2 + 34, x3 + 12}
          U41_A(x1,x2,x3) = max{x1 + 20, x2 + 34, x3 + 12}
          U31_A(x1,x2) = max{x1 + 9, x2 + 10}
          U21_A(x1) = x1
          U12_A(x1) = x1 + 17
          a__U11_A(x1,x2) = max{x1 + 11, x2 + 31}
          a__U12_A(x1) = x1 + 17
          a__U21_A(x1) = x1
          a__U31_A(x1,x2) = max{x1 + 9, x2 + 10}
          a__U41_A(x1,x2,x3) = max{x1 + 20, x2 + 34, x3 + 12}
          a__U42_A(x1,x2,x3) = max{x1 - 3, x2 + 34, x3 + 12}
          a__plus_A(x1,x2) = max{x1 + 12, x2 + 34}
          |0|_A = 16
          isNat_A(x1) = max{13, x1 - 2}
    
      precedence:
      
        mark# = U11 = s = plus = a__plus# = mark = a__U41# = a__isNat = tt = a__U42# = U42 = U41 = U31 = U21 = U12 = a__U11 = a__U12 = a__U21 = a__U31 = a__U41 = a__U42 = a__plus = |0| = isNat
      
      partial status:
    
        pi(mark#) = []
        pi(U11) = []
        pi(s) = []
        pi(plus) = []
        pi(a__plus#) = []
        pi(mark) = []
        pi(a__U41#) = []
        pi(a__isNat) = []
        pi(tt) = []
        pi(a__U42#) = []
        pi(U42) = []
        pi(U41) = []
        pi(U31) = []
        pi(U21) = []
        pi(U12) = []
        pi(a__U11) = []
        pi(a__U12) = []
        pi(a__U21) = []
        pi(a__U31) = []
        pi(a__U41) = []
        pi(a__U42) = []
        pi(a__plus) = []
        pi(|0|) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 72
          U11_A(x1,x2) = 19
          s_A(x1) = 21
          plus_A(x1,x2) = 10
          a__plus#_A(x1,x2) = 72
          mark_A(x1) = x1 + 23
          a__U41#_A(x1,x2,x3) = 72
          a__isNat_A(x1) = 20
          tt_A = 12
          a__U42#_A(x1,x2,x3) = 72
          U42_A(x1,x2,x3) = 23
          U41_A(x1,x2,x3) = 9
          U31_A(x1,x2) = 18
          U21_A(x1) = 19
          U12_A(x1) = 19
          a__U11_A(x1,x2) = 42
          a__U12_A(x1) = 41
          a__U21_A(x1) = 20
          a__U31_A(x1,x2) = 19
          a__U41_A(x1,x2,x3) = 32
          a__U42_A(x1,x2,x3) = 23
          a__plus_A(x1,x2) = 32
          |0|_A = 21
          isNat_A(x1) = 20
    
      precedence:
      
        |0| > mark = a__plus > plus > mark# = a__plus# = a__U41# = a__isNat = a__U42# = isNat > U41 = a__U41 = a__U42 > a__U21 > U42 > U21 = a__U31 > a__U11 > U31 > U12 = a__U12 > U11 = s = tt
      
      partial status:
    
        pi(mark#) = []
        pi(U11) = []
        pi(s) = []
        pi(plus) = []
        pi(a__plus#) = []
        pi(mark) = [1]
        pi(a__U41#) = []
        pi(a__isNat) = []
        pi(tt) = []
        pi(a__U42#) = []
        pi(U42) = []
        pi(U41) = []
        pi(U31) = []
        pi(U21) = []
        pi(U12) = []
        pi(a__U11) = []
        pi(a__U12) = []
        pi(a__U21) = []
        pi(a__U31) = []
        pi(a__U41) = []
        pi(a__U42) = []
        pi(a__plus) = []
        pi(|0|) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p5

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(U11(X1,X2)) -> mark#(X1)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(plus(X1,X2)) -> mark#(X2)
p4: mark#(plus(X1,X2)) -> mark#(X1)
p5: a__plus#(N,s(M)) -> a__U41#(a__isNat(M),M,N)
p6: a__U41#(tt(),M,N) -> a__U42#(a__isNat(N),M,N)
p7: a__U42#(tt(),M,N) -> mark#(N)
p8: mark#(U42(X1,X2,X3)) -> a__U42#(mark(X1),X2,X3)
p9: a__U42#(tt(),M,N) -> a__plus#(mark(N),mark(M))
p10: mark#(U41(X1,X2,X3)) -> mark#(X1)
p11: mark#(U31(X1,X2)) -> mark#(X1)
p12: mark#(U21(X)) -> mark#(X)
p13: mark#(U12(X)) -> mark#(X)

and R consists of:

r1: a__U11(tt(),V2) -> a__U12(a__isNat(V2))
r2: a__U12(tt()) -> tt()
r3: a__U21(tt()) -> tt()
r4: a__U31(tt(),N) -> mark(N)
r5: a__U41(tt(),M,N) -> a__U42(a__isNat(N),M,N)
r6: a__U42(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r7: a__isNat(|0|()) -> tt()
r8: a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
r9: a__isNat(s(V1)) -> a__U21(a__isNat(V1))
r10: a__plus(N,|0|()) -> a__U31(a__isNat(N),N)
r11: a__plus(N,s(M)) -> a__U41(a__isNat(M),M,N)
r12: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r13: mark(U12(X)) -> a__U12(mark(X))
r14: mark(isNat(X)) -> a__isNat(X)
r15: mark(U21(X)) -> a__U21(mark(X))
r16: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r17: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r18: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r19: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r20: mark(tt()) -> tt()
r21: mark(s(X)) -> s(mark(X))
r22: mark(|0|()) -> |0|()
r23: a__U11(X1,X2) -> U11(X1,X2)
r24: a__U12(X) -> U12(X)
r25: a__isNat(X) -> isNat(X)
r26: a__U21(X) -> U21(X)
r27: a__U31(X1,X2) -> U31(X1,X2)
r28: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r29: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r30: a__plus(X1,X2) -> plus(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13}


-- Reduction pair.

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

p1: mark#(U11(X1,X2)) -> mark#(X1)
p2: mark#(U12(X)) -> mark#(X)
p3: mark#(U21(X)) -> mark#(X)
p4: mark#(U31(X1,X2)) -> mark#(X1)
p5: mark#(U41(X1,X2,X3)) -> mark#(X1)
p6: mark#(U42(X1,X2,X3)) -> a__U42#(mark(X1),X2,X3)
p7: a__U42#(tt(),M,N) -> a__plus#(mark(N),mark(M))
p8: a__plus#(N,s(M)) -> a__U41#(a__isNat(M),M,N)
p9: a__U41#(tt(),M,N) -> a__U42#(a__isNat(N),M,N)
p10: a__U42#(tt(),M,N) -> mark#(N)
p11: mark#(plus(X1,X2)) -> mark#(X1)
p12: mark#(plus(X1,X2)) -> mark#(X2)
p13: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__U11(tt(),V2) -> a__U12(a__isNat(V2))
r2: a__U12(tt()) -> tt()
r3: a__U21(tt()) -> tt()
r4: a__U31(tt(),N) -> mark(N)
r5: a__U41(tt(),M,N) -> a__U42(a__isNat(N),M,N)
r6: a__U42(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r7: a__isNat(|0|()) -> tt()
r8: a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
r9: a__isNat(s(V1)) -> a__U21(a__isNat(V1))
r10: a__plus(N,|0|()) -> a__U31(a__isNat(N),N)
r11: a__plus(N,s(M)) -> a__U41(a__isNat(M),M,N)
r12: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r13: mark(U12(X)) -> a__U12(mark(X))
r14: mark(isNat(X)) -> a__isNat(X)
r15: mark(U21(X)) -> a__U21(mark(X))
r16: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r17: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r18: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r19: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r20: mark(tt()) -> tt()
r21: mark(s(X)) -> s(mark(X))
r22: mark(|0|()) -> |0|()
r23: a__U11(X1,X2) -> U11(X1,X2)
r24: a__U12(X) -> U12(X)
r25: a__isNat(X) -> isNat(X)
r26: a__U21(X) -> U21(X)
r27: a__U31(X1,X2) -> U31(X1,X2)
r28: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r29: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r30: a__plus(X1,X2) -> plus(X1,X2)

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, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{14, x1 - 1}
          U11_A(x1,x2) = max{x1 + 1, x2 + 14}
          U12_A(x1) = max{5, x1 + 2}
          U21_A(x1) = max{1, x1}
          U31_A(x1,x2) = max{28, x1 + 20, x2 + 24}
          U41_A(x1,x2,x3) = max{27, x1 + 20, x2 + 22, x3 + 24}
          U42_A(x1,x2,x3) = max{27, x1 + 23, x2 + 22, x3 + 24}
          a__U42#_A(x1,x2,x3) = max{13, x1 + 11, x2 + 9, x3 + 5}
          mark_A(x1) = max{3, x1}
          tt_A = 3
          a__plus#_A(x1,x2) = max{14, x1 + 5, x2 + 9}
          s_A(x1) = x1
          a__U41#_A(x1,x2,x3) = max{x1 + 11, x2 + 9, x3 + 5}
          a__isNat_A(x1) = max{3, x1 - 7}
          plus_A(x1,x2) = max{27, x1 + 24, x2 + 22}
          a__U11_A(x1,x2) = max{x1 + 1, x2 + 14}
          a__U12_A(x1) = max{5, x1 + 2}
          a__U21_A(x1) = max{2, x1}
          a__U31_A(x1,x2) = max{28, x1 + 20, x2 + 24}
          a__U41_A(x1,x2,x3) = max{27, x1 + 20, x2 + 22, x3 + 24}
          a__U42_A(x1,x2,x3) = max{27, x1 + 23, x2 + 22, x3 + 24}
          a__plus_A(x1,x2) = max{27, x1 + 24, x2 + 22}
          |0|_A = 11
          isNat_A(x1) = max{3, x1 - 7}
    
      precedence:
      
        mark > a__plus > a__isNat > U41 = a__U41 > a__U42 > s > a__U11 > U42 = a__U21 > U21 > a__U42# = a__plus# = a__U41# = plus = isNat > tt > a__U12 > mark# > U12 = a__U31 > |0| > U11 > U31
      
      partial status:
    
        pi(mark#) = []
        pi(U11) = []
        pi(U12) = []
        pi(U21) = []
        pi(U31) = []
        pi(U41) = [1]
        pi(U42) = [3]
        pi(a__U42#) = []
        pi(mark) = []
        pi(tt) = []
        pi(a__plus#) = []
        pi(s) = []
        pi(a__U41#) = []
        pi(a__isNat) = []
        pi(plus) = []
        pi(a__U11) = [1, 2]
        pi(a__U12) = [1]
        pi(a__U21) = []
        pi(a__U31) = []
        pi(a__U41) = [1]
        pi(a__U42) = []
        pi(a__plus) = []
        pi(|0|) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 5
          U11_A(x1,x2) = 5
          U12_A(x1) = 1
          U21_A(x1) = 4
          U31_A(x1,x2) = 6
          U41_A(x1,x2,x3) = max{6, x1 - 31}
          U42_A(x1,x2,x3) = 4
          a__U42#_A(x1,x2,x3) = 5
          mark_A(x1) = 13
          tt_A = 9
          a__plus#_A(x1,x2) = 5
          s_A(x1) = 5
          a__U41#_A(x1,x2,x3) = 5
          a__isNat_A(x1) = 39
          plus_A(x1,x2) = 5
          a__U11_A(x1,x2) = x1 + 41
          a__U12_A(x1) = max{2, x1}
          a__U21_A(x1) = 13
          a__U31_A(x1,x2) = 13
          a__U41_A(x1,x2,x3) = max{13, x1 - 28}
          a__U42_A(x1,x2,x3) = 8
          a__plus_A(x1,x2) = 13
          |0|_A = 14
          isNat_A(x1) = 1
    
      precedence:
      
        mark > s = a__U21 = a__U41 = a__plus > plus > mark# = U11 = U42 = a__U42# = a__plus# = a__U41# > a__isNat > U21 = U31 = U41 = a__U31 = a__U42 = |0| > isNat > a__U11 > a__U12 > tt > U12
      
      partial status:
    
        pi(mark#) = []
        pi(U11) = []
        pi(U12) = []
        pi(U21) = []
        pi(U31) = []
        pi(U41) = []
        pi(U42) = []
        pi(a__U42#) = []
        pi(mark) = []
        pi(tt) = []
        pi(a__plus#) = []
        pi(s) = []
        pi(a__U41#) = []
        pi(a__isNat) = []
        pi(plus) = []
        pi(a__U11) = []
        pi(a__U12) = []
        pi(a__U21) = []
        pi(a__U31) = []
        pi(a__U41) = []
        pi(a__U42) = []
        pi(a__plus) = []
        pi(|0|) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p10

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(U11(X1,X2)) -> mark#(X1)
p2: mark#(U12(X)) -> mark#(X)
p3: mark#(U21(X)) -> mark#(X)
p4: mark#(U31(X1,X2)) -> mark#(X1)
p5: mark#(U41(X1,X2,X3)) -> mark#(X1)
p6: mark#(U42(X1,X2,X3)) -> a__U42#(mark(X1),X2,X3)
p7: a__U42#(tt(),M,N) -> a__plus#(mark(N),mark(M))
p8: a__plus#(N,s(M)) -> a__U41#(a__isNat(M),M,N)
p9: a__U41#(tt(),M,N) -> a__U42#(a__isNat(N),M,N)
p10: mark#(plus(X1,X2)) -> mark#(X1)
p11: mark#(plus(X1,X2)) -> mark#(X2)
p12: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__U11(tt(),V2) -> a__U12(a__isNat(V2))
r2: a__U12(tt()) -> tt()
r3: a__U21(tt()) -> tt()
r4: a__U31(tt(),N) -> mark(N)
r5: a__U41(tt(),M,N) -> a__U42(a__isNat(N),M,N)
r6: a__U42(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r7: a__isNat(|0|()) -> tt()
r8: a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
r9: a__isNat(s(V1)) -> a__U21(a__isNat(V1))
r10: a__plus(N,|0|()) -> a__U31(a__isNat(N),N)
r11: a__plus(N,s(M)) -> a__U41(a__isNat(M),M,N)
r12: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r13: mark(U12(X)) -> a__U12(mark(X))
r14: mark(isNat(X)) -> a__isNat(X)
r15: mark(U21(X)) -> a__U21(mark(X))
r16: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r17: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r18: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r19: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r20: mark(tt()) -> tt()
r21: mark(s(X)) -> s(mark(X))
r22: mark(|0|()) -> |0|()
r23: a__U11(X1,X2) -> U11(X1,X2)
r24: a__U12(X) -> U12(X)
r25: a__isNat(X) -> isNat(X)
r26: a__U21(X) -> U21(X)
r27: a__U31(X1,X2) -> U31(X1,X2)
r28: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r29: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r30: a__plus(X1,X2) -> plus(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p10, p11, p12}
  {p7, p8, p9}


-- Reduction pair.

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

p1: mark#(U11(X1,X2)) -> mark#(X1)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(plus(X1,X2)) -> mark#(X2)
p4: mark#(plus(X1,X2)) -> mark#(X1)
p5: mark#(U41(X1,X2,X3)) -> mark#(X1)
p6: mark#(U31(X1,X2)) -> mark#(X1)
p7: mark#(U21(X)) -> mark#(X)
p8: mark#(U12(X)) -> mark#(X)

and R consists of:

r1: a__U11(tt(),V2) -> a__U12(a__isNat(V2))
r2: a__U12(tt()) -> tt()
r3: a__U21(tt()) -> tt()
r4: a__U31(tt(),N) -> mark(N)
r5: a__U41(tt(),M,N) -> a__U42(a__isNat(N),M,N)
r6: a__U42(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r7: a__isNat(|0|()) -> tt()
r8: a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
r9: a__isNat(s(V1)) -> a__U21(a__isNat(V1))
r10: a__plus(N,|0|()) -> a__U31(a__isNat(N),N)
r11: a__plus(N,s(M)) -> a__U41(a__isNat(M),M,N)
r12: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r13: mark(U12(X)) -> a__U12(mark(X))
r14: mark(isNat(X)) -> a__isNat(X)
r15: mark(U21(X)) -> a__U21(mark(X))
r16: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r17: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r18: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r19: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r20: mark(tt()) -> tt()
r21: mark(s(X)) -> s(mark(X))
r22: mark(|0|()) -> |0|()
r23: a__U11(X1,X2) -> U11(X1,X2)
r24: a__U12(X) -> U12(X)
r25: a__isNat(X) -> isNat(X)
r26: a__U21(X) -> U21(X)
r27: a__U31(X1,X2) -> U31(X1,X2)
r28: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r29: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r30: a__plus(X1,X2) -> plus(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{3, x1 + 2}
          U11_A(x1,x2) = max{x1, x2}
          s_A(x1) = max{1, x1}
          plus_A(x1,x2) = max{x1, x2}
          U41_A(x1,x2,x3) = max{1, x1, x3}
          U31_A(x1,x2) = max{x1, x2}
          U21_A(x1) = max{1, x1}
          U12_A(x1) = max{1, x1}
    
      precedence:
      
        mark# = U11 = s = plus = U41 = U31 = U21 = U12
      
      partial status:
    
        pi(mark#) = [1]
        pi(U11) = [1, 2]
        pi(s) = [1]
        pi(plus) = [1, 2]
        pi(U41) = [1, 3]
        pi(U31) = [1, 2]
        pi(U21) = [1]
        pi(U12) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{3, x1 + 2}
          U11_A(x1,x2) = max{x1, x2}
          s_A(x1) = x1 + 1
          plus_A(x1,x2) = max{x1, x2}
          U41_A(x1,x2,x3) = max{x1, x3}
          U31_A(x1,x2) = max{x1, x2}
          U21_A(x1) = x1 + 1
          U12_A(x1) = x1 + 1
    
      precedence:
      
        mark# = U11 = s = plus = U41 = U31 = U21 = U12
      
      partial status:
    
        pi(mark#) = [1]
        pi(U11) = [1, 2]
        pi(s) = [1]
        pi(plus) = [1, 2]
        pi(U41) = [1, 3]
        pi(U31) = [1, 2]
        pi(U21) = [1]
        pi(U12) = [1]
    

The next rules are strictly ordered:

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

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

-- Reduction pair.

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

p1: a__U42#(tt(),M,N) -> a__plus#(mark(N),mark(M))
p2: a__plus#(N,s(M)) -> a__U41#(a__isNat(M),M,N)
p3: a__U41#(tt(),M,N) -> a__U42#(a__isNat(N),M,N)

and R consists of:

r1: a__U11(tt(),V2) -> a__U12(a__isNat(V2))
r2: a__U12(tt()) -> tt()
r3: a__U21(tt()) -> tt()
r4: a__U31(tt(),N) -> mark(N)
r5: a__U41(tt(),M,N) -> a__U42(a__isNat(N),M,N)
r6: a__U42(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r7: a__isNat(|0|()) -> tt()
r8: a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
r9: a__isNat(s(V1)) -> a__U21(a__isNat(V1))
r10: a__plus(N,|0|()) -> a__U31(a__isNat(N),N)
r11: a__plus(N,s(M)) -> a__U41(a__isNat(M),M,N)
r12: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r13: mark(U12(X)) -> a__U12(mark(X))
r14: mark(isNat(X)) -> a__isNat(X)
r15: mark(U21(X)) -> a__U21(mark(X))
r16: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r17: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r18: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r19: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r20: mark(tt()) -> tt()
r21: mark(s(X)) -> s(mark(X))
r22: mark(|0|()) -> |0|()
r23: a__U11(X1,X2) -> U11(X1,X2)
r24: a__U12(X) -> U12(X)
r25: a__isNat(X) -> isNat(X)
r26: a__U21(X) -> U21(X)
r27: a__U31(X1,X2) -> U31(X1,X2)
r28: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r29: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r30: a__plus(X1,X2) -> plus(X1,X2)

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, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            a__U42#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + (4,5)
            tt_A() = (8,4)
            a__plus#_A(x1,x2) = ((1,0),(0,0)) x2 + (3,5)
            mark_A(x1) = ((1,0),(1,0)) x1 + (0,3)
            s_A(x1) = ((1,0),(0,0)) x1 + (4,1)
            a__U41#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + (5,5)
            a__isNat_A(x1) = ((1,0),(1,0)) x1 + (6,5)
            a__U11_A(x1,x2) = ((1,0),(1,0)) x2 + (7,10)
            a__U12_A(x1) = x1 + (1,1)
            a__U21_A(x1) = (9,4)
            a__U31_A(x1,x2) = ((1,0),(1,0)) x2 + (18,3)
            a__U41_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (13,2)
            a__U42_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (13,2)
            a__plus_A(x1,x2) = ((1,0),(1,0)) x1 + x2 + (9,1)
            |0|_A() = (9,4)
            U11_A(x1,x2) = ((1,0),(0,0)) x2 + (7,1)
            U12_A(x1) = ((1,0),(0,0)) x1 + (1,1)
            U21_A(x1) = (9,1)
            U31_A(x1,x2) = ((1,0),(1,0)) x2 + (18,3)
            U41_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (13,2)
            U42_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (13,1)
            plus_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (9,1)
            isNat_A(x1) = ((1,0),(0,0)) x1 + (6,1)
    
      precedence:
      
        a__U42# > mark > a__plus# = a__U41 = a__plus > a__U42 > a__U41# > U41 > s > a__isNat > plus > a__U11 > a__U12 = U12 > tt > a__U21 > isNat > a__U31 = U31 > |0| > U21 > U42 > U11
      
      partial status:
    
        pi(a__U42#) = []
        pi(tt) = []
        pi(a__plus#) = []
        pi(mark) = []
        pi(s) = []
        pi(a__U41#) = []
        pi(a__isNat) = []
        pi(a__U11) = []
        pi(a__U12) = [1]
        pi(a__U21) = []
        pi(a__U31) = []
        pi(a__U41) = []
        pi(a__U42) = []
        pi(a__plus) = [2]
        pi(|0|) = []
        pi(U11) = []
        pi(U12) = []
        pi(U21) = []
        pi(U31) = []
        pi(U41) = []
        pi(U42) = []
        pi(plus) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            a__U42#_A(x1,x2,x3) = (4,3)
            tt_A() = (0,2)
            a__plus#_A(x1,x2) = (3,3)
            mark_A(x1) = (4,3)
            s_A(x1) = (1,2)
            a__U41#_A(x1,x2,x3) = (2,2)
            a__isNat_A(x1) = (0,2)
            a__U11_A(x1,x2) = (0,2)
            a__U12_A(x1) = ((1,0),(1,1)) x1
            a__U21_A(x1) = (0,2)
            a__U31_A(x1,x2) = (4,3)
            a__U41_A(x1,x2,x3) = (3,3)
            a__U42_A(x1,x2,x3) = (2,2)
            a__plus_A(x1,x2) = ((0,0),(1,1)) x2 + (4,0)
            |0|_A() = (1,0)
            U11_A(x1,x2) = (1,0)
            U12_A(x1) = (0,0)
            U21_A(x1) = (0,0)
            U31_A(x1,x2) = (4,0)
            U41_A(x1,x2,x3) = (0,0)
            U42_A(x1,x2,x3) = (2,0)
            plus_A(x1,x2) = (1,0)
            isNat_A(x1) = (0,0)
    
      precedence:
      
        a__U42# > mark = a__U31 = a__plus > |0| > U31 > a__plus# > a__U41# > a__isNat = a__U21 = U21 > isNat > a__U41 > U41 > plus > a__U11 > U11 > tt = a__U12 > s = a__U42 > U12 = U42
      
      partial status:
    
        pi(a__U42#) = []
        pi(tt) = []
        pi(a__plus#) = []
        pi(mark) = []
        pi(s) = []
        pi(a__U41#) = []
        pi(a__isNat) = []
        pi(a__U11) = []
        pi(a__U12) = [1]
        pi(a__U21) = []
        pi(a__U31) = []
        pi(a__U41) = []
        pi(a__U42) = []
        pi(a__plus) = []
        pi(|0|) = []
        pi(U11) = []
        pi(U12) = []
        pi(U21) = []
        pi(U31) = []
        pi(U41) = []
        pi(U42) = []
        pi(plus) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p1, p2, p3

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

-- Reduction pair.

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

p1: a__U11#(tt(),V2) -> a__isNat#(V2)
p2: a__isNat#(s(V1)) -> a__isNat#(V1)
p3: a__isNat#(plus(V1,V2)) -> a__isNat#(V1)
p4: a__isNat#(plus(V1,V2)) -> a__U11#(a__isNat(V1),V2)

and R consists of:

r1: a__U11(tt(),V2) -> a__U12(a__isNat(V2))
r2: a__U12(tt()) -> tt()
r3: a__U21(tt()) -> tt()
r4: a__U31(tt(),N) -> mark(N)
r5: a__U41(tt(),M,N) -> a__U42(a__isNat(N),M,N)
r6: a__U42(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r7: a__isNat(|0|()) -> tt()
r8: a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
r9: a__isNat(s(V1)) -> a__U21(a__isNat(V1))
r10: a__plus(N,|0|()) -> a__U31(a__isNat(N),N)
r11: a__plus(N,s(M)) -> a__U41(a__isNat(M),M,N)
r12: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r13: mark(U12(X)) -> a__U12(mark(X))
r14: mark(isNat(X)) -> a__isNat(X)
r15: mark(U21(X)) -> a__U21(mark(X))
r16: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r17: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r18: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r19: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r20: mark(tt()) -> tt()
r21: mark(s(X)) -> s(mark(X))
r22: mark(|0|()) -> |0|()
r23: a__U11(X1,X2) -> U11(X1,X2)
r24: a__U12(X) -> U12(X)
r25: a__isNat(X) -> isNat(X)
r26: a__U21(X) -> U21(X)
r27: a__U31(X1,X2) -> U31(X1,X2)
r28: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r29: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r30: a__plus(X1,X2) -> plus(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r7, r8, r9, r23, r24, r25, r26

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__U11#_A(x1,x2) = max{x1 + 2, x2 + 3}
          tt_A = 9
          a__isNat#_A(x1) = x1 + 3
          s_A(x1) = x1 + 7
          plus_A(x1,x2) = max{x1 + 9, x2 + 5}
          a__isNat_A(x1) = x1 + 6
          a__U12_A(x1) = max{5, x1}
          U12_A(x1) = max{5, x1}
          a__U11_A(x1,x2) = max{10, x1 + 6, x2 + 6}
          a__U21_A(x1) = max{8, x1 + 4}
          U11_A(x1,x2) = max{x1 + 6, x2 + 6}
          U21_A(x1) = x1 + 4
          |0|_A = 10
          isNat_A(x1) = x1 + 6
    
      precedence:
      
        a__U11# = tt = plus = a__U11 > a__isNat# = s = a__isNat = a__U12 > U12 = a__U21 = U11 = isNat > U21 = |0|
      
      partial status:
    
        pi(a__U11#) = [1, 2]
        pi(tt) = []
        pi(a__isNat#) = [1]
        pi(s) = [1]
        pi(plus) = [1, 2]
        pi(a__isNat) = [1]
        pi(a__U12) = [1]
        pi(U12) = [1]
        pi(a__U11) = [1, 2]
        pi(a__U21) = [1]
        pi(U11) = [1, 2]
        pi(U21) = [1]
        pi(|0|) = []
        pi(isNat) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__U11#_A(x1,x2) = max{x1 - 6, x2 + 7}
          tt_A = 12
          a__isNat#_A(x1) = x1 + 6
          s_A(x1) = x1 + 2
          plus_A(x1,x2) = max{x1 + 1, x2 + 2}
          a__isNat_A(x1) = max{10, x1 + 8}
          a__U12_A(x1) = max{15, x1 + 5}
          U12_A(x1) = max{16, x1 + 6}
          a__U11_A(x1,x2) = max{x1 + 2, x2 + 11}
          a__U21_A(x1) = max{11, x1 + 3}
          U11_A(x1,x2) = max{x1 + 3, x2 + 12}
          U21_A(x1) = max{12, x1 + 4}
          |0|_A = 11
          isNat_A(x1) = max{11, x1 + 9}
    
      precedence:
      
        a__U11# = tt = a__isNat# = s = plus = a__isNat = a__U12 = U12 = a__U11 = a__U21 = U11 = U21 = |0| = isNat
      
      partial status:
    
        pi(a__U11#) = []
        pi(tt) = []
        pi(a__isNat#) = []
        pi(s) = [1]
        pi(plus) = [2]
        pi(a__isNat) = [1]
        pi(a__U12) = [1]
        pi(U12) = []
        pi(a__U11) = []
        pi(a__U21) = []
        pi(U11) = []
        pi(U21) = []
        pi(|0|) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p1, p2, p3, p4

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