YES

We show the termination of the TRS R:

  U11(tt(),V2) -> U12(isNat(activate(V2)))
  U12(tt()) -> tt()
  U21(tt()) -> tt()
  U31(tt(),N) -> activate(N)
  U41(tt(),M,N) -> U42(isNat(activate(N)),activate(M),activate(N))
  U42(tt(),M,N) -> s(plus(activate(N),activate(M)))
  isNat(n__0()) -> tt()
  isNat(n__plus(V1,V2)) -> U11(isNat(activate(V1)),activate(V2))
  isNat(n__s(V1)) -> U21(isNat(activate(V1)))
  plus(N,|0|()) -> U31(isNat(N),N)
  plus(N,s(M)) -> U41(isNat(M),M,N)
  |0|() -> n__0()
  plus(X1,X2) -> n__plus(X1,X2)
  s(X) -> n__s(X)
  activate(n__0()) -> |0|()
  activate(n__plus(X1,X2)) -> plus(X1,X2)
  activate(n__s(X)) -> s(X)
  activate(X) -> X

-- SCC decomposition.

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

p1: U11#(tt(),V2) -> U12#(isNat(activate(V2)))
p2: U11#(tt(),V2) -> isNat#(activate(V2))
p3: U11#(tt(),V2) -> activate#(V2)
p4: U31#(tt(),N) -> activate#(N)
p5: U41#(tt(),M,N) -> U42#(isNat(activate(N)),activate(M),activate(N))
p6: U41#(tt(),M,N) -> isNat#(activate(N))
p7: U41#(tt(),M,N) -> activate#(N)
p8: U41#(tt(),M,N) -> activate#(M)
p9: U42#(tt(),M,N) -> s#(plus(activate(N),activate(M)))
p10: U42#(tt(),M,N) -> plus#(activate(N),activate(M))
p11: U42#(tt(),M,N) -> activate#(N)
p12: U42#(tt(),M,N) -> activate#(M)
p13: isNat#(n__plus(V1,V2)) -> U11#(isNat(activate(V1)),activate(V2))
p14: isNat#(n__plus(V1,V2)) -> isNat#(activate(V1))
p15: isNat#(n__plus(V1,V2)) -> activate#(V1)
p16: isNat#(n__plus(V1,V2)) -> activate#(V2)
p17: isNat#(n__s(V1)) -> U21#(isNat(activate(V1)))
p18: isNat#(n__s(V1)) -> isNat#(activate(V1))
p19: isNat#(n__s(V1)) -> activate#(V1)
p20: plus#(N,|0|()) -> U31#(isNat(N),N)
p21: plus#(N,|0|()) -> isNat#(N)
p22: plus#(N,s(M)) -> U41#(isNat(M),M,N)
p23: plus#(N,s(M)) -> isNat#(M)
p24: activate#(n__0()) -> |0|#()
p25: activate#(n__plus(X1,X2)) -> plus#(X1,X2)
p26: activate#(n__s(X)) -> s#(X)

and R consists of:

r1: U11(tt(),V2) -> U12(isNat(activate(V2)))
r2: U12(tt()) -> tt()
r3: U21(tt()) -> tt()
r4: U31(tt(),N) -> activate(N)
r5: U41(tt(),M,N) -> U42(isNat(activate(N)),activate(M),activate(N))
r6: U42(tt(),M,N) -> s(plus(activate(N),activate(M)))
r7: isNat(n__0()) -> tt()
r8: isNat(n__plus(V1,V2)) -> U11(isNat(activate(V1)),activate(V2))
r9: isNat(n__s(V1)) -> U21(isNat(activate(V1)))
r10: plus(N,|0|()) -> U31(isNat(N),N)
r11: plus(N,s(M)) -> U41(isNat(M),M,N)
r12: |0|() -> n__0()
r13: plus(X1,X2) -> n__plus(X1,X2)
r14: s(X) -> n__s(X)
r15: activate(n__0()) -> |0|()
r16: activate(n__plus(X1,X2)) -> plus(X1,X2)
r17: activate(n__s(X)) -> s(X)
r18: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p2, p3, p4, p5, p6, p7, p8, p10, p11, p12, p13, p14, p15, p16, p18, p19, p20, p21, p22, p23, p25}


-- Reduction pair.

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

p1: U11#(tt(),V2) -> isNat#(activate(V2))
p2: isNat#(n__s(V1)) -> activate#(V1)
p3: activate#(n__plus(X1,X2)) -> plus#(X1,X2)
p4: plus#(N,s(M)) -> isNat#(M)
p5: isNat#(n__s(V1)) -> isNat#(activate(V1))
p6: isNat#(n__plus(V1,V2)) -> activate#(V2)
p7: isNat#(n__plus(V1,V2)) -> activate#(V1)
p8: isNat#(n__plus(V1,V2)) -> isNat#(activate(V1))
p9: isNat#(n__plus(V1,V2)) -> U11#(isNat(activate(V1)),activate(V2))
p10: U11#(tt(),V2) -> activate#(V2)
p11: plus#(N,s(M)) -> U41#(isNat(M),M,N)
p12: U41#(tt(),M,N) -> activate#(M)
p13: U41#(tt(),M,N) -> activate#(N)
p14: U41#(tt(),M,N) -> isNat#(activate(N))
p15: U41#(tt(),M,N) -> U42#(isNat(activate(N)),activate(M),activate(N))
p16: U42#(tt(),M,N) -> activate#(M)
p17: U42#(tt(),M,N) -> activate#(N)
p18: U42#(tt(),M,N) -> plus#(activate(N),activate(M))
p19: plus#(N,|0|()) -> isNat#(N)
p20: plus#(N,|0|()) -> U31#(isNat(N),N)
p21: U31#(tt(),N) -> activate#(N)

and R consists of:

r1: U11(tt(),V2) -> U12(isNat(activate(V2)))
r2: U12(tt()) -> tt()
r3: U21(tt()) -> tt()
r4: U31(tt(),N) -> activate(N)
r5: U41(tt(),M,N) -> U42(isNat(activate(N)),activate(M),activate(N))
r6: U42(tt(),M,N) -> s(plus(activate(N),activate(M)))
r7: isNat(n__0()) -> tt()
r8: isNat(n__plus(V1,V2)) -> U11(isNat(activate(V1)),activate(V2))
r9: isNat(n__s(V1)) -> U21(isNat(activate(V1)))
r10: plus(N,|0|()) -> U31(isNat(N),N)
r11: plus(N,s(M)) -> U41(isNat(M),M,N)
r12: |0|() -> n__0()
r13: plus(X1,X2) -> n__plus(X1,X2)
r14: s(X) -> n__s(X)
r15: activate(n__0()) -> |0|()
r16: activate(n__plus(X1,X2)) -> plus(X1,X2)
r17: activate(n__s(X)) -> s(X)
r18: activate(X) -> 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          U11#_A(x1,x2) = max{x1 - 15, x2 + 19}
          tt_A = 25
          isNat#_A(x1) = x1 + 18
          activate_A(x1) = x1
          n__s_A(x1) = max{28, x1}
          activate#_A(x1) = x1 + 17
          n__plus_A(x1,x2) = max{27, x1 + 22, x2 + 20}
          plus#_A(x1,x2) = max{x1 + 36, x2 + 36}
          s_A(x1) = max{28, x1}
          isNat_A(x1) = x1 + 36
          U41#_A(x1,x2,x3) = max{x1 - 17, x2 + 36, x3 + 36}
          U42#_A(x1,x2,x3) = max{x1 - 9, x2 + 36, x3 + 36}
          |0|_A = 9
          U31#_A(x1,x2) = max{x1 - 1, x2 + 18}
          U42_A(x1,x2,x3) = max{28, x2 + 20, x3 + 22}
          plus_A(x1,x2) = max{27, x1 + 22, x2 + 20}
          U12_A(x1) = 52
          U31_A(x1,x2) = max{21, x1 - 15, x2 + 1}
          U41_A(x1,x2,x3) = max{37, x2 + 20, x3 + 22}
          U11_A(x1,x2) = x2 + 56
          U21_A(x1) = max{36, x1 - 35}
          n__0_A = 9
    
      precedence:
      
        U11# = tt = isNat# = activate = n__s = activate# = n__plus = plus# = s = isNat = U41# = U42# = |0| = U31# = U42 = plus = U12 = U31 = U41 = U11 = U21 = n__0
      
      partial status:
    
        pi(U11#) = []
        pi(tt) = []
        pi(isNat#) = []
        pi(activate) = []
        pi(n__s) = []
        pi(activate#) = []
        pi(n__plus) = []
        pi(plus#) = []
        pi(s) = []
        pi(isNat) = []
        pi(U41#) = []
        pi(U42#) = []
        pi(|0|) = []
        pi(U31#) = []
        pi(U42) = []
        pi(plus) = []
        pi(U12) = []
        pi(U31) = []
        pi(U41) = []
        pi(U11) = []
        pi(U21) = []
        pi(n__0) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          U11#_A(x1,x2) = 10
          tt_A = 11
          isNat#_A(x1) = 10
          activate_A(x1) = max{104, x1 + 64}
          n__s_A(x1) = 41
          activate#_A(x1) = 10
          n__plus_A(x1,x2) = 160
          plus#_A(x1,x2) = 10
          s_A(x1) = 105
          isNat_A(x1) = 103
          U41#_A(x1,x2,x3) = 10
          U42#_A(x1,x2,x3) = 10
          |0|_A = 105
          U31#_A(x1,x2) = 9
          U42_A(x1,x2,x3) = 223
          plus_A(x1,x2) = 224
          U12_A(x1) = 102
          U31_A(x1,x2) = 223
          U41_A(x1,x2,x3) = 223
          U11_A(x1,x2) = 103
          U21_A(x1) = 10
          n__0_A = 41
    
      precedence:
      
        activate > n__s = s = isNat > tt > activate# = plus# = U41# = U42# > |0| > U31# > U11# = isNat# > plus = U41 > n__plus = U12 = U11 = U21 = n__0 > U42 = U31
      
      partial status:
    
        pi(U11#) = []
        pi(tt) = []
        pi(isNat#) = []
        pi(activate) = []
        pi(n__s) = []
        pi(activate#) = []
        pi(n__plus) = []
        pi(plus#) = []
        pi(s) = []
        pi(isNat) = []
        pi(U41#) = []
        pi(U42#) = []
        pi(|0|) = []
        pi(U31#) = []
        pi(U42) = []
        pi(plus) = []
        pi(U12) = []
        pi(U31) = []
        pi(U41) = []
        pi(U11) = []
        pi(U21) = []
        pi(n__0) = []
    

The next rules are strictly ordered:

  p2, p6, p7, p10, p19, p21

We remove them from the problem.

-- SCC decomposition.

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

p1: U11#(tt(),V2) -> isNat#(activate(V2))
p2: activate#(n__plus(X1,X2)) -> plus#(X1,X2)
p3: plus#(N,s(M)) -> isNat#(M)
p4: isNat#(n__s(V1)) -> isNat#(activate(V1))
p5: isNat#(n__plus(V1,V2)) -> isNat#(activate(V1))
p6: isNat#(n__plus(V1,V2)) -> U11#(isNat(activate(V1)),activate(V2))
p7: plus#(N,s(M)) -> U41#(isNat(M),M,N)
p8: U41#(tt(),M,N) -> activate#(M)
p9: U41#(tt(),M,N) -> activate#(N)
p10: U41#(tt(),M,N) -> isNat#(activate(N))
p11: U41#(tt(),M,N) -> U42#(isNat(activate(N)),activate(M),activate(N))
p12: U42#(tt(),M,N) -> activate#(M)
p13: U42#(tt(),M,N) -> activate#(N)
p14: U42#(tt(),M,N) -> plus#(activate(N),activate(M))
p15: plus#(N,|0|()) -> U31#(isNat(N),N)

and R consists of:

r1: U11(tt(),V2) -> U12(isNat(activate(V2)))
r2: U12(tt()) -> tt()
r3: U21(tt()) -> tt()
r4: U31(tt(),N) -> activate(N)
r5: U41(tt(),M,N) -> U42(isNat(activate(N)),activate(M),activate(N))
r6: U42(tt(),M,N) -> s(plus(activate(N),activate(M)))
r7: isNat(n__0()) -> tt()
r8: isNat(n__plus(V1,V2)) -> U11(isNat(activate(V1)),activate(V2))
r9: isNat(n__s(V1)) -> U21(isNat(activate(V1)))
r10: plus(N,|0|()) -> U31(isNat(N),N)
r11: plus(N,s(M)) -> U41(isNat(M),M,N)
r12: |0|() -> n__0()
r13: plus(X1,X2) -> n__plus(X1,X2)
r14: s(X) -> n__s(X)
r15: activate(n__0()) -> |0|()
r16: activate(n__plus(X1,X2)) -> plus(X1,X2)
r17: activate(n__s(X)) -> s(X)
r18: activate(X) -> X

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: plus#(N,s(M)) -> U41#(isNat(M),M,N)
p2: U41#(tt(),M,N) -> U42#(isNat(activate(N)),activate(M),activate(N))
p3: U42#(tt(),M,N) -> plus#(activate(N),activate(M))
p4: U42#(tt(),M,N) -> activate#(N)
p5: activate#(n__plus(X1,X2)) -> plus#(X1,X2)
p6: U42#(tt(),M,N) -> activate#(M)
p7: U41#(tt(),M,N) -> activate#(N)
p8: U41#(tt(),M,N) -> activate#(M)

and R consists of:

r1: U11(tt(),V2) -> U12(isNat(activate(V2)))
r2: U12(tt()) -> tt()
r3: U21(tt()) -> tt()
r4: U31(tt(),N) -> activate(N)
r5: U41(tt(),M,N) -> U42(isNat(activate(N)),activate(M),activate(N))
r6: U42(tt(),M,N) -> s(plus(activate(N),activate(M)))
r7: isNat(n__0()) -> tt()
r8: isNat(n__plus(V1,V2)) -> U11(isNat(activate(V1)),activate(V2))
r9: isNat(n__s(V1)) -> U21(isNat(activate(V1)))
r10: plus(N,|0|()) -> U31(isNat(N),N)
r11: plus(N,s(M)) -> U41(isNat(M),M,N)
r12: |0|() -> n__0()
r13: plus(X1,X2) -> n__plus(X1,X2)
r14: s(X) -> n__s(X)
r15: activate(n__0()) -> |0|()
r16: activate(n__plus(X1,X2)) -> plus(X1,X2)
r17: activate(n__s(X)) -> s(X)
r18: activate(X) -> 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          plus#_A(x1,x2) = max{x1 + 21, x2 + 22}
          s_A(x1) = max{13, x1}
          U41#_A(x1,x2,x3) = max{x1 + 2, x2 + 22, x3 + 21}
          isNat_A(x1) = max{0, x1 - 3}
          tt_A = 8
          U42#_A(x1,x2,x3) = max{x1 + 11, x2 + 22, x3 + 21}
          activate_A(x1) = x1
          activate#_A(x1) = max{20, x1 - 1}
          n__plus_A(x1,x2) = max{x1 + 22, x2 + 27}
          U42_A(x1,x2,x3) = max{x2 + 27, x3 + 22}
          plus_A(x1,x2) = max{x1 + 22, x2 + 27}
          U12_A(x1) = 9
          U31_A(x1,x2) = max{39, x1 + 4, x2}
          U41_A(x1,x2,x3) = max{40, x1 + 20, x2 + 27, x3 + 22}
          U11_A(x1,x2) = max{10, x1 + 2}
          U21_A(x1) = max{9, x1 - 1}
          |0|_A = 12
          n__0_A = 12
          n__s_A(x1) = max{13, x1}
    
      precedence:
      
        activate# > plus# = U41# = U42# = |0| = n__0 > U21 > n__plus = plus > U41 > U31 = U11 > U12 > U42 > s = activate > n__s > isNat = tt
      
      partial status:
    
        pi(plus#) = []
        pi(s) = []
        pi(U41#) = []
        pi(isNat) = []
        pi(tt) = []
        pi(U42#) = []
        pi(activate) = [1]
        pi(activate#) = []
        pi(n__plus) = []
        pi(U42) = []
        pi(plus) = []
        pi(U12) = []
        pi(U31) = [1, 2]
        pi(U41) = [3]
        pi(U11) = []
        pi(U21) = []
        pi(|0|) = []
        pi(n__0) = []
        pi(n__s) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          plus#_A(x1,x2) = 72
          s_A(x1) = 37
          U41#_A(x1,x2,x3) = 72
          isNat_A(x1) = 21
          tt_A = 18
          U42#_A(x1,x2,x3) = 72
          activate_A(x1) = 37
          activate#_A(x1) = 49
          n__plus_A(x1,x2) = 37
          U42_A(x1,x2,x3) = 37
          plus_A(x1,x2) = 37
          U12_A(x1) = 1
          U31_A(x1,x2) = max{x1 + 20, x2 + 39}
          U41_A(x1,x2,x3) = 37
          U11_A(x1,x2) = 52
          U21_A(x1) = 1
          |0|_A = 63
          n__0_A = 61
          n__s_A(x1) = 24
    
      precedence:
      
        activate > n__s > s > plus# = U41# = U42# > isNat = activate# = U21 = |0| = n__0 > tt = U11 > plus = U31 > U41 > n__plus = U42 = U12
      
      partial status:
    
        pi(plus#) = []
        pi(s) = []
        pi(U41#) = []
        pi(isNat) = []
        pi(tt) = []
        pi(U42#) = []
        pi(activate) = []
        pi(activate#) = []
        pi(n__plus) = []
        pi(U42) = []
        pi(plus) = []
        pi(U12) = []
        pi(U31) = [2]
        pi(U41) = []
        pi(U11) = []
        pi(U21) = []
        pi(|0|) = []
        pi(n__0) = []
        pi(n__s) = []
    

The next rules are strictly ordered:

  p5, p6, p8

We remove them from the problem.

-- SCC decomposition.

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

p1: plus#(N,s(M)) -> U41#(isNat(M),M,N)
p2: U41#(tt(),M,N) -> U42#(isNat(activate(N)),activate(M),activate(N))
p3: U42#(tt(),M,N) -> plus#(activate(N),activate(M))
p4: U42#(tt(),M,N) -> activate#(N)
p5: U41#(tt(),M,N) -> activate#(N)

and R consists of:

r1: U11(tt(),V2) -> U12(isNat(activate(V2)))
r2: U12(tt()) -> tt()
r3: U21(tt()) -> tt()
r4: U31(tt(),N) -> activate(N)
r5: U41(tt(),M,N) -> U42(isNat(activate(N)),activate(M),activate(N))
r6: U42(tt(),M,N) -> s(plus(activate(N),activate(M)))
r7: isNat(n__0()) -> tt()
r8: isNat(n__plus(V1,V2)) -> U11(isNat(activate(V1)),activate(V2))
r9: isNat(n__s(V1)) -> U21(isNat(activate(V1)))
r10: plus(N,|0|()) -> U31(isNat(N),N)
r11: plus(N,s(M)) -> U41(isNat(M),M,N)
r12: |0|() -> n__0()
r13: plus(X1,X2) -> n__plus(X1,X2)
r14: s(X) -> n__s(X)
r15: activate(n__0()) -> |0|()
r16: activate(n__plus(X1,X2)) -> plus(X1,X2)
r17: activate(n__s(X)) -> s(X)
r18: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- Reduction pair.

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

p1: plus#(N,s(M)) -> U41#(isNat(M),M,N)
p2: U41#(tt(),M,N) -> U42#(isNat(activate(N)),activate(M),activate(N))
p3: U42#(tt(),M,N) -> plus#(activate(N),activate(M))

and R consists of:

r1: U11(tt(),V2) -> U12(isNat(activate(V2)))
r2: U12(tt()) -> tt()
r3: U21(tt()) -> tt()
r4: U31(tt(),N) -> activate(N)
r5: U41(tt(),M,N) -> U42(isNat(activate(N)),activate(M),activate(N))
r6: U42(tt(),M,N) -> s(plus(activate(N),activate(M)))
r7: isNat(n__0()) -> tt()
r8: isNat(n__plus(V1,V2)) -> U11(isNat(activate(V1)),activate(V2))
r9: isNat(n__s(V1)) -> U21(isNat(activate(V1)))
r10: plus(N,|0|()) -> U31(isNat(N),N)
r11: plus(N,s(M)) -> U41(isNat(M),M,N)
r12: |0|() -> n__0()
r13: plus(X1,X2) -> n__plus(X1,X2)
r14: s(X) -> n__s(X)
r15: activate(n__0()) -> |0|()
r16: activate(n__plus(X1,X2)) -> plus(X1,X2)
r17: activate(n__s(X)) -> s(X)
r18: activate(X) -> 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            plus#_A(x1,x2) = x2 + (10,0)
            s_A(x1) = x1 + (18,35)
            U41#_A(x1,x2,x3) = x2 + (18,4)
            isNat_A(x1) = ((0,0),(0,1)) x1 + (33,0)
            tt_A() = (31,0)
            U42#_A(x1,x2,x3) = x2 + (14,2)
            activate_A(x1) = x1 + (4,2)
            U42_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((0,1),(1,1)) x2 + x3 + (31,14)
            plus_A(x1,x2) = x1 + ((0,1),(1,1)) x2 + (6,2)
            U12_A(x1) = (32,1)
            U31_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (5,0)
            U41_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((0,1),(1,1)) x2 + x3 + (7,55)
            U11_A(x1,x2) = (33,1)
            U21_A(x1) = (32,35)
            |0|_A() = (34,0)
            n__0_A() = (32,0)
            n__plus_A(x1,x2) = x1 + ((0,1),(1,1)) x2 + (3,1)
            n__s_A(x1) = x1 + (18,35)
    
      precedence:
      
        isNat > U11 > U12 = U21 > tt = n__0 > U42 > s = n__s > U41# > U42# > plus# > activate = U31 > plus > |0| > U41 > n__plus
      
      partial status:
    
        pi(plus#) = [2]
        pi(s) = []
        pi(U41#) = [2]
        pi(isNat) = []
        pi(tt) = []
        pi(U42#) = [2]
        pi(activate) = []
        pi(U42) = []
        pi(plus) = []
        pi(U12) = []
        pi(U31) = [2]
        pi(U41) = []
        pi(U11) = []
        pi(U21) = []
        pi(|0|) = []
        pi(n__0) = []
        pi(n__plus) = []
        pi(n__s) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            plus#_A(x1,x2) = ((1,0),(1,0)) x2 + (1,0)
            s_A(x1) = (20,1)
            U41#_A(x1,x2,x3) = (19,9)
            isNat_A(x1) = (5,0)
            tt_A() = (2,0)
            U42#_A(x1,x2,x3) = x2 + (10,8)
            activate_A(x1) = (8,1)
            U42_A(x1,x2,x3) = (5,1)
            plus_A(x1,x2) = (7,1)
            U12_A(x1) = (3,0)
            U31_A(x1,x2) = ((0,1),(0,1)) x2 + (9,2)
            U41_A(x1,x2,x3) = (6,1)
            U11_A(x1,x2) = (4,0)
            U21_A(x1) = (3,0)
            |0|_A() = (1,1)
            n__0_A() = (1,0)
            n__plus_A(x1,x2) = (0,0)
            n__s_A(x1) = (20,1)
    
      precedence:
      
        |0| > n__0 > U21 > U41 > U31 > activate > U41# > U42# = plus > isNat > U11 > U12 > tt > plus# = s = U42 = n__plus = n__s
      
      partial status:
    
        pi(plus#) = []
        pi(s) = []
        pi(U41#) = []
        pi(isNat) = []
        pi(tt) = []
        pi(U42#) = [2]
        pi(activate) = []
        pi(U42) = []
        pi(plus) = []
        pi(U12) = []
        pi(U31) = []
        pi(U41) = []
        pi(U11) = []
        pi(U21) = []
        pi(|0|) = []
        pi(n__0) = []
        pi(n__plus) = []
        pi(n__s) = []
    

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: U11#(tt(),V2) -> isNat#(activate(V2))
p2: isNat#(n__plus(V1,V2)) -> U11#(isNat(activate(V1)),activate(V2))
p3: isNat#(n__plus(V1,V2)) -> isNat#(activate(V1))
p4: isNat#(n__s(V1)) -> isNat#(activate(V1))

and R consists of:

r1: U11(tt(),V2) -> U12(isNat(activate(V2)))
r2: U12(tt()) -> tt()
r3: U21(tt()) -> tt()
r4: U31(tt(),N) -> activate(N)
r5: U41(tt(),M,N) -> U42(isNat(activate(N)),activate(M),activate(N))
r6: U42(tt(),M,N) -> s(plus(activate(N),activate(M)))
r7: isNat(n__0()) -> tt()
r8: isNat(n__plus(V1,V2)) -> U11(isNat(activate(V1)),activate(V2))
r9: isNat(n__s(V1)) -> U21(isNat(activate(V1)))
r10: plus(N,|0|()) -> U31(isNat(N),N)
r11: plus(N,s(M)) -> U41(isNat(M),M,N)
r12: |0|() -> n__0()
r13: plus(X1,X2) -> n__plus(X1,X2)
r14: s(X) -> n__s(X)
r15: activate(n__0()) -> |0|()
r16: activate(n__plus(X1,X2)) -> plus(X1,X2)
r17: activate(n__s(X)) -> s(X)
r18: activate(X) -> 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          U11#_A(x1,x2) = max{x1, x2}
          tt_A = 0
          isNat#_A(x1) = max{0, x1 - 3}
          activate_A(x1) = x1
          n__plus_A(x1,x2) = max{x1 + 12, x2 + 14}
          isNat_A(x1) = max{0, x1 - 3}
          n__s_A(x1) = max{15, x1}
          U42_A(x1,x2,x3) = max{x1 + 15, x2 + 14, x3 + 12}
          s_A(x1) = max{15, x1}
          plus_A(x1,x2) = max{x1 + 12, x2 + 14}
          U12_A(x1) = max{6, x1 + 4}
          U31_A(x1,x2) = max{x1, x2}
          U41_A(x1,x2,x3) = max{x1 + 16, x2 + 14, x3 + 12}
          U11_A(x1,x2) = max{x1 + 8, x2 + 7}
          U21_A(x1) = max{1, x1 - 4}
          |0|_A = 4
          n__0_A = 4
    
      precedence:
      
        U21 > U31 > activate = plus > U41 > n__plus = isNat > tt = n__s = U42 = s = U12 = U11 > U11# = isNat# = |0| = n__0
      
      partial status:
    
        pi(U11#) = [1, 2]
        pi(tt) = []
        pi(isNat#) = []
        pi(activate) = [1]
        pi(n__plus) = []
        pi(isNat) = []
        pi(n__s) = []
        pi(U42) = [1]
        pi(s) = []
        pi(plus) = [2]
        pi(U12) = [1]
        pi(U31) = [1, 2]
        pi(U41) = [2, 3]
        pi(U11) = [2]
        pi(U21) = []
        pi(|0|) = []
        pi(n__0) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          U11#_A(x1,x2) = max{x1 + 76, x2 + 88}
          tt_A = 58
          isNat#_A(x1) = 88
          activate_A(x1) = 0
          n__plus_A(x1,x2) = 0
          isNat_A(x1) = 12
          n__s_A(x1) = 4
          U42_A(x1,x2,x3) = max{0, x1 - 12}
          s_A(x1) = 11
          plus_A(x1,x2) = 0
          U12_A(x1) = x1 + 82
          U31_A(x1,x2) = max{47, x1 + 35, x2 + 9}
          U41_A(x1,x2,x3) = 0
          U11_A(x1,x2) = x2 + 37
          U21_A(x1) = 13
          |0|_A = 1
          n__0_A = 0
    
      precedence:
      
        U31 = U11 = U21 = |0| > isNat = s > tt > n__0 > isNat# > U11# > activate = n__s = U12 > plus > U41 > n__plus = U42
      
      partial status:
    
        pi(U11#) = []
        pi(tt) = []
        pi(isNat#) = []
        pi(activate) = []
        pi(n__plus) = []
        pi(isNat) = []
        pi(n__s) = []
        pi(U42) = []
        pi(s) = []
        pi(plus) = []
        pi(U12) = []
        pi(U31) = [2]
        pi(U41) = []
        pi(U11) = []
        pi(U21) = []
        pi(|0|) = []
        pi(n__0) = []
    

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: isNat#(n__plus(V1,V2)) -> U11#(isNat(activate(V1)),activate(V2))
p2: isNat#(n__plus(V1,V2)) -> isNat#(activate(V1))
p3: isNat#(n__s(V1)) -> isNat#(activate(V1))

and R consists of:

r1: U11(tt(),V2) -> U12(isNat(activate(V2)))
r2: U12(tt()) -> tt()
r3: U21(tt()) -> tt()
r4: U31(tt(),N) -> activate(N)
r5: U41(tt(),M,N) -> U42(isNat(activate(N)),activate(M),activate(N))
r6: U42(tt(),M,N) -> s(plus(activate(N),activate(M)))
r7: isNat(n__0()) -> tt()
r8: isNat(n__plus(V1,V2)) -> U11(isNat(activate(V1)),activate(V2))
r9: isNat(n__s(V1)) -> U21(isNat(activate(V1)))
r10: plus(N,|0|()) -> U31(isNat(N),N)
r11: plus(N,s(M)) -> U41(isNat(M),M,N)
r12: |0|() -> n__0()
r13: plus(X1,X2) -> n__plus(X1,X2)
r14: s(X) -> n__s(X)
r15: activate(n__0()) -> |0|()
r16: activate(n__plus(X1,X2)) -> plus(X1,X2)
r17: activate(n__s(X)) -> s(X)
r18: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p2, p3}


-- Reduction pair.

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

p1: isNat#(n__plus(V1,V2)) -> isNat#(activate(V1))
p2: isNat#(n__s(V1)) -> isNat#(activate(V1))

and R consists of:

r1: U11(tt(),V2) -> U12(isNat(activate(V2)))
r2: U12(tt()) -> tt()
r3: U21(tt()) -> tt()
r4: U31(tt(),N) -> activate(N)
r5: U41(tt(),M,N) -> U42(isNat(activate(N)),activate(M),activate(N))
r6: U42(tt(),M,N) -> s(plus(activate(N),activate(M)))
r7: isNat(n__0()) -> tt()
r8: isNat(n__plus(V1,V2)) -> U11(isNat(activate(V1)),activate(V2))
r9: isNat(n__s(V1)) -> U21(isNat(activate(V1)))
r10: plus(N,|0|()) -> U31(isNat(N),N)
r11: plus(N,s(M)) -> U41(isNat(M),M,N)
r12: |0|() -> n__0()
r13: plus(X1,X2) -> n__plus(X1,X2)
r14: s(X) -> n__s(X)
r15: activate(n__0()) -> |0|()
r16: activate(n__plus(X1,X2)) -> plus(X1,X2)
r17: activate(n__s(X)) -> s(X)
r18: activate(X) -> 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          isNat#_A(x1) = max{14, x1 - 3}
          n__plus_A(x1,x2) = max{x1 + 13, x2 + 25}
          activate_A(x1) = max{15, x1}
          n__s_A(x1) = max{14, x1}
          U12_A(x1) = 22
          tt_A = 12
          U11_A(x1,x2) = max{12, x1 + 10}
          isNat_A(x1) = x1 + 5
          U21_A(x1) = 15
          U42_A(x1,x2,x3) = max{40, x1 + 4, x2 + 25, x3 + 13}
          s_A(x1) = max{15, x1}
          plus_A(x1,x2) = max{x1 + 13, x2 + 25}
          U31_A(x1,x2) = max{x1 + 3, x2 + 12}
          U41_A(x1,x2,x3) = max{40, x2 + 25, x3 + 13}
          n__0_A = 13
          |0|_A = 14
    
      precedence:
      
        activate = U11 = isNat = U42 = s = plus = U31 = U41 = |0| > n__plus > U21 > n__0 > isNat# = n__s = U12 = tt
      
      partial status:
    
        pi(isNat#) = []
        pi(n__plus) = [1]
        pi(activate) = [1]
        pi(n__s) = []
        pi(U12) = []
        pi(tt) = []
        pi(U11) = []
        pi(isNat) = [1]
        pi(U21) = []
        pi(U42) = []
        pi(s) = []
        pi(plus) = [1, 2]
        pi(U31) = [2]
        pi(U41) = [3]
        pi(n__0) = []
        pi(|0|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          isNat#_A(x1) = 60
          n__plus_A(x1,x2) = max{56, x1 + 54}
          activate_A(x1) = max{8, x1 + 2}
          n__s_A(x1) = 5
          U12_A(x1) = 56
          tt_A = 21
          U11_A(x1,x2) = 57
          isNat_A(x1) = x1 + 37
          U21_A(x1) = 47
          U42_A(x1,x2,x3) = 60
          s_A(x1) = 8
          plus_A(x1,x2) = max{57, x1 + 54}
          U31_A(x1,x2) = max{53, x2 + 2}
          U41_A(x1,x2,x3) = x3 + 54
          n__0_A = 10
          |0|_A = 9
    
      precedence:
      
        isNat# = U31 > activate = n__s = U12 = tt = U11 = isNat = U21 = U42 = s = plus = U41 = n__0 = |0| > n__plus
      
      partial status:
    
        pi(isNat#) = []
        pi(n__plus) = []
        pi(activate) = [1]
        pi(n__s) = []
        pi(U12) = []
        pi(tt) = []
        pi(U11) = []
        pi(isNat) = []
        pi(U21) = []
        pi(U42) = []
        pi(s) = []
        pi(plus) = []
        pi(U31) = []
        pi(U41) = []
        pi(n__0) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: isNat#(n__s(V1)) -> isNat#(activate(V1))

and R consists of:

r1: U11(tt(),V2) -> U12(isNat(activate(V2)))
r2: U12(tt()) -> tt()
r3: U21(tt()) -> tt()
r4: U31(tt(),N) -> activate(N)
r5: U41(tt(),M,N) -> U42(isNat(activate(N)),activate(M),activate(N))
r6: U42(tt(),M,N) -> s(plus(activate(N),activate(M)))
r7: isNat(n__0()) -> tt()
r8: isNat(n__plus(V1,V2)) -> U11(isNat(activate(V1)),activate(V2))
r9: isNat(n__s(V1)) -> U21(isNat(activate(V1)))
r10: plus(N,|0|()) -> U31(isNat(N),N)
r11: plus(N,s(M)) -> U41(isNat(M),M,N)
r12: |0|() -> n__0()
r13: plus(X1,X2) -> n__plus(X1,X2)
r14: s(X) -> n__s(X)
r15: activate(n__0()) -> |0|()
r16: activate(n__plus(X1,X2)) -> plus(X1,X2)
r17: activate(n__s(X)) -> s(X)
r18: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: isNat#(n__s(V1)) -> isNat#(activate(V1))

and R consists of:

r1: U11(tt(),V2) -> U12(isNat(activate(V2)))
r2: U12(tt()) -> tt()
r3: U21(tt()) -> tt()
r4: U31(tt(),N) -> activate(N)
r5: U41(tt(),M,N) -> U42(isNat(activate(N)),activate(M),activate(N))
r6: U42(tt(),M,N) -> s(plus(activate(N),activate(M)))
r7: isNat(n__0()) -> tt()
r8: isNat(n__plus(V1,V2)) -> U11(isNat(activate(V1)),activate(V2))
r9: isNat(n__s(V1)) -> U21(isNat(activate(V1)))
r10: plus(N,|0|()) -> U31(isNat(N),N)
r11: plus(N,s(M)) -> U41(isNat(M),M,N)
r12: |0|() -> n__0()
r13: plus(X1,X2) -> n__plus(X1,X2)
r14: s(X) -> n__s(X)
r15: activate(n__0()) -> |0|()
r16: activate(n__plus(X1,X2)) -> plus(X1,X2)
r17: activate(n__s(X)) -> s(X)
r18: activate(X) -> 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            isNat#_A(x1) = ((1,0),(1,1)) x1 + (86,16)
            n__s_A(x1) = x1 + (87,20)
            activate_A(x1) = x1 + (2,3)
            U12_A(x1) = (60,3)
            tt_A() = (59,2)
            U11_A(x1,x2) = x1 + x2 + (42,42)
            isNat_A(x1) = ((1,0),(1,1)) x1 + (84,39)
            U21_A(x1) = x1 + (2,0)
            U42_A(x1,x2,x3) = ((1,1),(1,1)) x2 + ((1,1),(0,1)) x3 + (147,35)
            s_A(x1) = x1 + (88,23)
            plus_A(x1,x2) = ((1,1),(0,1)) x1 + ((1,1),(1,1)) x2 + (48,4)
            U31_A(x1,x2) = x2 + (3,5)
            U41_A(x1,x2,x3) = ((1,1),(1,1)) x2 + ((1,1),(0,1)) x3 + (158,43)
            n__0_A() = (30,1)
            n__plus_A(x1,x2) = ((1,1),(0,1)) x1 + ((1,1),(1,1)) x2 + (47,3)
            |0|_A() = (31,4)
    
      precedence:
      
        plus = U31 = U41 = n__plus > U42 = s > n__s > isNat# > n__0 > isNat > U21 > U12 = tt = U11 > activate = |0|
      
      partial status:
    
        pi(isNat#) = [1]
        pi(n__s) = [1]
        pi(activate) = [1]
        pi(U12) = []
        pi(tt) = []
        pi(U11) = [1]
        pi(isNat) = [1]
        pi(U21) = [1]
        pi(U42) = [2]
        pi(s) = []
        pi(plus) = [2]
        pi(U31) = []
        pi(U41) = []
        pi(n__0) = []
        pi(n__plus) = []
        pi(|0|) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            isNat#_A(x1) = x1 + (1,0)
            n__s_A(x1) = ((1,1),(0,1)) x1 + (9,4)
            activate_A(x1) = (7,4)
            U12_A(x1) = (4,3)
            tt_A() = (3,2)
            U11_A(x1,x2) = (5,3)
            isNat_A(x1) = ((1,1),(0,1)) x1 + (0,5)
            U21_A(x1) = (0,0)
            U42_A(x1,x2,x3) = (2,1)
            s_A(x1) = (1,1)
            plus_A(x1,x2) = (7,4)
            U31_A(x1,x2) = (7,4)
            U41_A(x1,x2,x3) = (6,4)
            n__0_A() = (7,1)
            n__plus_A(x1,x2) = (6,3)
            |0|_A() = (7,4)
    
      precedence:
      
        tt > U41 > U42 > n__s = U21 = s > activate = U11 = isNat = plus = U31 = n__0 = n__plus = |0| > isNat# > U12
      
      partial status:
    
        pi(isNat#) = [1]
        pi(n__s) = [1]
        pi(activate) = []
        pi(U12) = []
        pi(tt) = []
        pi(U11) = []
        pi(isNat) = [1]
        pi(U21) = []
        pi(U42) = []
        pi(s) = []
        pi(plus) = []
        pi(U31) = []
        pi(U41) = []
        pi(n__0) = []
        pi(n__plus) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p1

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