YES

We show the termination of the TRS R:

  U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
  U12(tt(),V2) -> U13(isNat(activate(V2)))
  U13(tt()) -> tt()
  U21(tt(),V1) -> U22(isNat(activate(V1)))
  U22(tt()) -> tt()
  U31(tt(),N) -> activate(N)
  U41(tt(),M,N) -> s(plus(activate(N),activate(M)))
  and(tt(),X) -> activate(X)
  isNat(n__0()) -> tt()
  isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))
  isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
  isNatKind(n__0()) -> tt()
  isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
  isNatKind(n__s(V1)) -> isNatKind(activate(V1))
  plus(N,|0|()) -> U31(and(isNat(N),n__isNatKind(N)),N)
  plus(N,s(M)) -> U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
  |0|() -> n__0()
  plus(X1,X2) -> n__plus(X1,X2)
  isNatKind(X) -> n__isNatKind(X)
  s(X) -> n__s(X)
  and(X1,X2) -> n__and(X1,X2)
  activate(n__0()) -> |0|()
  activate(n__plus(X1,X2)) -> plus(X1,X2)
  activate(n__isNatKind(X)) -> isNatKind(X)
  activate(n__s(X)) -> s(X)
  activate(n__and(X1,X2)) -> and(X1,X2)
  activate(X) -> X

-- SCC decomposition.

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

p1: U11#(tt(),V1,V2) -> U12#(isNat(activate(V1)),activate(V2))
p2: U11#(tt(),V1,V2) -> isNat#(activate(V1))
p3: U11#(tt(),V1,V2) -> activate#(V1)
p4: U11#(tt(),V1,V2) -> activate#(V2)
p5: U12#(tt(),V2) -> U13#(isNat(activate(V2)))
p6: U12#(tt(),V2) -> isNat#(activate(V2))
p7: U12#(tt(),V2) -> activate#(V2)
p8: U21#(tt(),V1) -> U22#(isNat(activate(V1)))
p9: U21#(tt(),V1) -> isNat#(activate(V1))
p10: U21#(tt(),V1) -> activate#(V1)
p11: U31#(tt(),N) -> activate#(N)
p12: U41#(tt(),M,N) -> s#(plus(activate(N),activate(M)))
p13: U41#(tt(),M,N) -> plus#(activate(N),activate(M))
p14: U41#(tt(),M,N) -> activate#(N)
p15: U41#(tt(),M,N) -> activate#(M)
p16: and#(tt(),X) -> activate#(X)
p17: isNat#(n__plus(V1,V2)) -> U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))
p18: isNat#(n__plus(V1,V2)) -> and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
p19: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p20: isNat#(n__plus(V1,V2)) -> activate#(V1)
p21: isNat#(n__plus(V1,V2)) -> activate#(V2)
p22: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p23: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p24: isNat#(n__s(V1)) -> activate#(V1)
p25: isNatKind#(n__plus(V1,V2)) -> and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
p26: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p27: isNatKind#(n__plus(V1,V2)) -> activate#(V1)
p28: isNatKind#(n__plus(V1,V2)) -> activate#(V2)
p29: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
p30: isNatKind#(n__s(V1)) -> activate#(V1)
p31: plus#(N,|0|()) -> U31#(and(isNat(N),n__isNatKind(N)),N)
p32: plus#(N,|0|()) -> and#(isNat(N),n__isNatKind(N))
p33: plus#(N,|0|()) -> isNat#(N)
p34: plus#(N,s(M)) -> U41#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
p35: plus#(N,s(M)) -> and#(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N)))
p36: plus#(N,s(M)) -> and#(isNat(M),n__isNatKind(M))
p37: plus#(N,s(M)) -> isNat#(M)
p38: plus#(N,s(M)) -> isNat#(N)
p39: activate#(n__0()) -> |0|#()
p40: activate#(n__plus(X1,X2)) -> plus#(X1,X2)
p41: activate#(n__isNatKind(X)) -> isNatKind#(X)
p42: activate#(n__s(X)) -> s#(X)
p43: activate#(n__and(X1,X2)) -> and#(X1,X2)

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
r2: U12(tt(),V2) -> U13(isNat(activate(V2)))
r3: U13(tt()) -> tt()
r4: U21(tt(),V1) -> U22(isNat(activate(V1)))
r5: U22(tt()) -> tt()
r6: U31(tt(),N) -> activate(N)
r7: U41(tt(),M,N) -> s(plus(activate(N),activate(M)))
r8: and(tt(),X) -> activate(X)
r9: isNat(n__0()) -> tt()
r10: isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))
r11: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r12: isNatKind(n__0()) -> tt()
r13: isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
r14: isNatKind(n__s(V1)) -> isNatKind(activate(V1))
r15: plus(N,|0|()) -> U31(and(isNat(N),n__isNatKind(N)),N)
r16: plus(N,s(M)) -> U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
r17: |0|() -> n__0()
r18: plus(X1,X2) -> n__plus(X1,X2)
r19: isNatKind(X) -> n__isNatKind(X)
r20: s(X) -> n__s(X)
r21: and(X1,X2) -> n__and(X1,X2)
r22: activate(n__0()) -> |0|()
r23: activate(n__plus(X1,X2)) -> plus(X1,X2)
r24: activate(n__isNatKind(X)) -> isNatKind(X)
r25: activate(n__s(X)) -> s(X)
r26: activate(n__and(X1,X2)) -> and(X1,X2)
r27: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p6, p7, p9, p10, p11, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32, p33, p34, p35, p36, p37, p38, p40, p41, p43}


-- Reduction pair.

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

p1: U11#(tt(),V1,V2) -> U12#(isNat(activate(V1)),activate(V2))
p2: U12#(tt(),V2) -> activate#(V2)
p3: activate#(n__and(X1,X2)) -> and#(X1,X2)
p4: and#(tt(),X) -> activate#(X)
p5: activate#(n__isNatKind(X)) -> isNatKind#(X)
p6: isNatKind#(n__s(V1)) -> activate#(V1)
p7: activate#(n__plus(X1,X2)) -> plus#(X1,X2)
p8: plus#(N,s(M)) -> isNat#(N)
p9: isNat#(n__s(V1)) -> activate#(V1)
p10: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p11: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
p12: isNatKind#(n__plus(V1,V2)) -> activate#(V2)
p13: isNatKind#(n__plus(V1,V2)) -> activate#(V1)
p14: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p15: isNatKind#(n__plus(V1,V2)) -> and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
p16: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p17: U21#(tt(),V1) -> activate#(V1)
p18: U21#(tt(),V1) -> isNat#(activate(V1))
p19: isNat#(n__plus(V1,V2)) -> activate#(V2)
p20: isNat#(n__plus(V1,V2)) -> activate#(V1)
p21: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p22: isNat#(n__plus(V1,V2)) -> and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
p23: isNat#(n__plus(V1,V2)) -> U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))
p24: U11#(tt(),V1,V2) -> activate#(V2)
p25: U11#(tt(),V1,V2) -> activate#(V1)
p26: U11#(tt(),V1,V2) -> isNat#(activate(V1))
p27: plus#(N,s(M)) -> isNat#(M)
p28: plus#(N,s(M)) -> and#(isNat(M),n__isNatKind(M))
p29: plus#(N,s(M)) -> and#(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N)))
p30: plus#(N,s(M)) -> U41#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
p31: U41#(tt(),M,N) -> activate#(M)
p32: U41#(tt(),M,N) -> activate#(N)
p33: U41#(tt(),M,N) -> plus#(activate(N),activate(M))
p34: plus#(N,|0|()) -> isNat#(N)
p35: plus#(N,|0|()) -> and#(isNat(N),n__isNatKind(N))
p36: plus#(N,|0|()) -> U31#(and(isNat(N),n__isNatKind(N)),N)
p37: U31#(tt(),N) -> activate#(N)
p38: U12#(tt(),V2) -> isNat#(activate(V2))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
r2: U12(tt(),V2) -> U13(isNat(activate(V2)))
r3: U13(tt()) -> tt()
r4: U21(tt(),V1) -> U22(isNat(activate(V1)))
r5: U22(tt()) -> tt()
r6: U31(tt(),N) -> activate(N)
r7: U41(tt(),M,N) -> s(plus(activate(N),activate(M)))
r8: and(tt(),X) -> activate(X)
r9: isNat(n__0()) -> tt()
r10: isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))
r11: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r12: isNatKind(n__0()) -> tt()
r13: isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
r14: isNatKind(n__s(V1)) -> isNatKind(activate(V1))
r15: plus(N,|0|()) -> U31(and(isNat(N),n__isNatKind(N)),N)
r16: plus(N,s(M)) -> U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
r17: |0|() -> n__0()
r18: plus(X1,X2) -> n__plus(X1,X2)
r19: isNatKind(X) -> n__isNatKind(X)
r20: s(X) -> n__s(X)
r21: and(X1,X2) -> n__and(X1,X2)
r22: activate(n__0()) -> |0|()
r23: activate(n__plus(X1,X2)) -> plus(X1,X2)
r24: activate(n__isNatKind(X)) -> isNatKind(X)
r25: activate(n__s(X)) -> s(X)
r26: activate(n__and(X1,X2)) -> and(X1,X2)
r27: 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, r19, r20, r21, r22, r23, r24, r25, r26, r27

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,x3) = max{x1, x2 + 172, x3 + 273}
          tt_A = 203
          U12#_A(x1,x2) = max{x1 - 48, x2 + 118}
          isNat_A(x1) = 206
          activate_A(x1) = max{53, x1}
          activate#_A(x1) = max{2, x1}
          n__and_A(x1,x2) = max{329, x1 + 5, x2 + 17}
          and#_A(x1,x2) = max{221, x1 + 4, x2 + 10}
          n__isNatKind_A(x1) = x1 + 167
          isNatKind#_A(x1) = x1 + 3
          n__s_A(x1) = max{227, x1}
          n__plus_A(x1,x2) = max{x1 + 226, x2 + 228}
          plus#_A(x1,x2) = max{x1 + 226, x2 + 222}
          s_A(x1) = max{227, x1}
          isNat#_A(x1) = x1 + 101
          isNatKind_A(x1) = x1 + 167
          U21#_A(x1,x2) = max{227, x1 - 120, x2 + 101}
          and_A(x1,x2) = max{329, x1 + 5, x2 + 17}
          U41#_A(x1,x2,x3) = max{279, x1 - 125, x2 + 222, x3 + 226}
          |0|_A = 38
          U31#_A(x1,x2) = max{78, x2 + 3}
          U13_A(x1) = 204
          U12_A(x1,x2) = max{204, x1 - 2}
          U22_A(x1) = max{204, x1 - 172}
          U31_A(x1,x2) = max{266, x1 - 183, x2 + 226}
          U41_A(x1,x2,x3) = max{282, x1 + 25, x2 + 228, x3 + 226}
          plus_A(x1,x2) = max{x1 + 226, x2 + 228}
          U11_A(x1,x2,x3) = 205
          U21_A(x1,x2) = 205
          n__0_A = 37
    
      precedence:
      
        isNat# = U21# > n__isNatKind = isNatKind > isNatKind# > n__plus = plus# = U41# = plus > U31# > U11# > U12# > n__and = and > activate# = and# > U11 > isNat > U41 > activate = s = U22 = U21 > U13 = U12 > n__s > U31 > |0| > tt > n__0
      
      partial status:
    
        pi(U11#) = [1]
        pi(tt) = []
        pi(U12#) = []
        pi(isNat) = []
        pi(activate) = [1]
        pi(activate#) = [1]
        pi(n__and) = [1, 2]
        pi(and#) = [1, 2]
        pi(n__isNatKind) = []
        pi(isNatKind#) = []
        pi(n__s) = []
        pi(n__plus) = []
        pi(plus#) = []
        pi(s) = []
        pi(isNat#) = []
        pi(isNatKind) = []
        pi(U21#) = []
        pi(and) = [1, 2]
        pi(U41#) = []
        pi(|0|) = []
        pi(U31#) = []
        pi(U13) = []
        pi(U12) = []
        pi(U22) = []
        pi(U31) = [2]
        pi(U41) = [1, 3]
        pi(plus) = []
        pi(U11) = []
        pi(U21) = []
        pi(n__0) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          U11#_A(x1,x2,x3) = max{19, x1 + 1}
          tt_A = 2277
          U12#_A(x1,x2) = 2089
          isNat_A(x1) = 2086
          activate_A(x1) = max{707, x1 + 699}
          activate#_A(x1) = 18
          n__and_A(x1,x2) = 1
          and#_A(x1,x2) = max{x1 + 1, x2 + 1008}
          n__isNatKind_A(x1) = 1079
          isNatKind#_A(x1) = 18
          n__s_A(x1) = 2088
          n__plus_A(x1,x2) = 20
          plus#_A(x1,x2) = 2087
          s_A(x1) = 1428
          isNat#_A(x1) = 2088
          isNatKind_A(x1) = 1785
          U21#_A(x1,x2) = 2088
          and_A(x1,x2) = max{x1 - 991, x2 + 706}
          U41#_A(x1,x2,x3) = 2087
          |0|_A = 653
          U31#_A(x1,x2) = 19
          U13_A(x1) = 2085
          U12_A(x1,x2) = 2086
          U22_A(x1) = 4648
          U31_A(x1,x2) = max{796, x2 + 699}
          U41_A(x1,x2,x3) = max{0, x1 - 774}
          plus_A(x1,x2) = 20
          U11_A(x1,x2,x3) = 2086
          U21_A(x1,x2) = 2085
          n__0_A = 208
    
      precedence:
      
        n__0 > |0| > n__and > isNatKind > activate = and > U11# = U12# > plus > tt > U21 > isNat = n__s = isNat# = U21# > activate# > plus# = U41# > and# > s = U13 = U41 > isNatKind# = U11 > U31# = U31 > U22 > n__isNatKind > n__plus = U12
      
      partial status:
    
        pi(U11#) = [1]
        pi(tt) = []
        pi(U12#) = []
        pi(isNat) = []
        pi(activate) = []
        pi(activate#) = []
        pi(n__and) = []
        pi(and#) = [1, 2]
        pi(n__isNatKind) = []
        pi(isNatKind#) = []
        pi(n__s) = []
        pi(n__plus) = []
        pi(plus#) = []
        pi(s) = []
        pi(isNat#) = []
        pi(isNatKind) = []
        pi(U21#) = []
        pi(and) = [2]
        pi(U41#) = []
        pi(|0|) = []
        pi(U31#) = []
        pi(U13) = []
        pi(U12) = []
        pi(U22) = []
        pi(U31) = []
        pi(U41) = []
        pi(plus) = []
        pi(U11) = []
        pi(U21) = []
        pi(n__0) = []
    

The next rules are strictly ordered:

  p2, p3, p4, p6, p7, p8, p12, p13, p15, p17, p19, p20, p22, p23, p24, p25, p26, p27, p28, p29, p31, p32, p34, p35, p36, p37, p38

We remove them from the problem.

-- SCC decomposition.

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

p1: U11#(tt(),V1,V2) -> U12#(isNat(activate(V1)),activate(V2))
p2: activate#(n__isNatKind(X)) -> isNatKind#(X)
p3: isNat#(n__s(V1)) -> activate#(V1)
p4: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p5: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
p6: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p7: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p8: U21#(tt(),V1) -> isNat#(activate(V1))
p9: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p10: plus#(N,s(M)) -> U41#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
p11: U41#(tt(),M,N) -> plus#(activate(N),activate(M))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
r2: U12(tt(),V2) -> U13(isNat(activate(V2)))
r3: U13(tt()) -> tt()
r4: U21(tt(),V1) -> U22(isNat(activate(V1)))
r5: U22(tt()) -> tt()
r6: U31(tt(),N) -> activate(N)
r7: U41(tt(),M,N) -> s(plus(activate(N),activate(M)))
r8: and(tt(),X) -> activate(X)
r9: isNat(n__0()) -> tt()
r10: isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))
r11: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r12: isNatKind(n__0()) -> tt()
r13: isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
r14: isNatKind(n__s(V1)) -> isNatKind(activate(V1))
r15: plus(N,|0|()) -> U31(and(isNat(N),n__isNatKind(N)),N)
r16: plus(N,s(M)) -> U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
r17: |0|() -> n__0()
r18: plus(X1,X2) -> n__plus(X1,X2)
r19: isNatKind(X) -> n__isNatKind(X)
r20: s(X) -> n__s(X)
r21: and(X1,X2) -> n__and(X1,X2)
r22: activate(n__0()) -> |0|()
r23: activate(n__plus(X1,X2)) -> plus(X1,X2)
r24: activate(n__isNatKind(X)) -> isNatKind(X)
r25: activate(n__s(X)) -> s(X)
r26: activate(n__and(X1,X2)) -> and(X1,X2)
r27: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p7, p8}
  {p5, p6}
  {p10, p11}


-- Reduction pair.

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

p1: U21#(tt(),V1) -> isNat#(activate(V1))
p2: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
r2: U12(tt(),V2) -> U13(isNat(activate(V2)))
r3: U13(tt()) -> tt()
r4: U21(tt(),V1) -> U22(isNat(activate(V1)))
r5: U22(tt()) -> tt()
r6: U31(tt(),N) -> activate(N)
r7: U41(tt(),M,N) -> s(plus(activate(N),activate(M)))
r8: and(tt(),X) -> activate(X)
r9: isNat(n__0()) -> tt()
r10: isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))
r11: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r12: isNatKind(n__0()) -> tt()
r13: isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
r14: isNatKind(n__s(V1)) -> isNatKind(activate(V1))
r15: plus(N,|0|()) -> U31(and(isNat(N),n__isNatKind(N)),N)
r16: plus(N,s(M)) -> U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
r17: |0|() -> n__0()
r18: plus(X1,X2) -> n__plus(X1,X2)
r19: isNatKind(X) -> n__isNatKind(X)
r20: s(X) -> n__s(X)
r21: and(X1,X2) -> n__and(X1,X2)
r22: activate(n__0()) -> |0|()
r23: activate(n__plus(X1,X2)) -> plus(X1,X2)
r24: activate(n__isNatKind(X)) -> isNatKind(X)
r25: activate(n__s(X)) -> s(X)
r26: activate(n__and(X1,X2)) -> and(X1,X2)
r27: 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, r19, r20, r21, r22, r23, r24, r25, r26, r27

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            U21#_A(x1,x2) = ((0,1),(0,1)) x2 + (332,9)
            tt_A() = (76,8)
            isNat#_A(x1) = ((0,1),(0,1)) x1 + (76,8)
            activate_A(x1) = x1 + (84,1)
            n__s_A(x1) = x1 + (87,258)
            isNatKind_A(x1) = ((0,1),(1,1)) x1 + (87,18)
            U13_A(x1) = (78,9)
            U12_A(x1,x2) = (80,9)
            isNat_A(x1) = ((0,0),(1,0)) x1 + (171,72)
            U22_A(x1) = (77,9)
            U11_A(x1,x2,x3) = ((0,0),(1,1)) x2 + (82,17)
            U21_A(x1,x2) = (171,9)
            U31_A(x1,x2) = ((1,0),(1,1)) x2 + (172,140)
            U41_A(x1,x2,x3) = ((0,1),(1,1)) x2 + ((1,1),(1,1)) x3 + (289,529)
            s_A(x1) = x1 + (170,258)
            plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,1),(1,1)) x2 + (33,101)
            n__0_A() = (74,139)
            n__plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,1),(1,1)) x2 + (31,101)
            and_A(x1,x2) = ((0,1),(0,0)) x1 + ((1,0),(1,1)) x2 + (77,42)
            n__isNatKind_A(x1) = ((0,1),(1,1)) x1 + (5,17)
            |0|_A() = (156,139)
            n__and_A(x1,x2) = ((0,1),(0,0)) x1 + ((1,0),(1,1)) x2 + (75,42)
    
      precedence:
      
        n__s > activate = |0| > U31 = U41 = s = plus > n__plus > and > isNatKind > tt = U13 = U12 = U22 > isNat > U21 > n__and > U21# = isNat# > U11 > n__0 > n__isNatKind
      
      partial status:
    
        pi(U21#) = []
        pi(tt) = []
        pi(isNat#) = []
        pi(activate) = []
        pi(n__s) = []
        pi(isNatKind) = []
        pi(U13) = []
        pi(U12) = []
        pi(isNat) = []
        pi(U22) = []
        pi(U11) = []
        pi(U21) = []
        pi(U31) = []
        pi(U41) = []
        pi(s) = []
        pi(plus) = []
        pi(n__0) = []
        pi(n__plus) = []
        pi(and) = []
        pi(n__isNatKind) = []
        pi(|0|) = []
        pi(n__and) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            U21#_A(x1,x2) = (7,6)
            tt_A() = (0,3)
            isNat#_A(x1) = (1,5)
            activate_A(x1) = (6,5)
            n__s_A(x1) = (1,0)
            isNatKind_A(x1) = (0,4)
            U13_A(x1) = (1,4)
            U12_A(x1,x2) = (7,4)
            isNat_A(x1) = (3,2)
            U22_A(x1) = (0,3)
            U11_A(x1,x2,x3) = (2,2)
            U21_A(x1,x2) = (1,1)
            U31_A(x1,x2) = (6,5)
            U41_A(x1,x2,x3) = (5,5)
            s_A(x1) = (4,3)
            plus_A(x1,x2) = (6,5)
            n__0_A() = (0,1)
            n__plus_A(x1,x2) = (1,4)
            and_A(x1,x2) = (0,4)
            n__isNatKind_A(x1) = (0,4)
            |0|_A() = (7,5)
            n__and_A(x1,x2) = (0,0)
    
      precedence:
      
        U11 > isNat# = activate = isNatKind = U13 = isNat = U21 = U31 = plus = and = n__and > U21# > n__isNatKind > s > n__s = U12 = U22 = n__0 = n__plus = |0| > tt = U41
      
      partial status:
    
        pi(U21#) = []
        pi(tt) = []
        pi(isNat#) = []
        pi(activate) = []
        pi(n__s) = []
        pi(isNatKind) = []
        pi(U13) = []
        pi(U12) = []
        pi(isNat) = []
        pi(U22) = []
        pi(U11) = []
        pi(U21) = []
        pi(U31) = []
        pi(U41) = []
        pi(s) = []
        pi(plus) = []
        pi(n__0) = []
        pi(n__plus) = []
        pi(and) = []
        pi(n__isNatKind) = []
        pi(|0|) = []
        pi(n__and) = []
    

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

p1: U21#(tt(),V1) -> isNat#(activate(V1))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
r2: U12(tt(),V2) -> U13(isNat(activate(V2)))
r3: U13(tt()) -> tt()
r4: U21(tt(),V1) -> U22(isNat(activate(V1)))
r5: U22(tt()) -> tt()
r6: U31(tt(),N) -> activate(N)
r7: U41(tt(),M,N) -> s(plus(activate(N),activate(M)))
r8: and(tt(),X) -> activate(X)
r9: isNat(n__0()) -> tt()
r10: isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))
r11: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r12: isNatKind(n__0()) -> tt()
r13: isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
r14: isNatKind(n__s(V1)) -> isNatKind(activate(V1))
r15: plus(N,|0|()) -> U31(and(isNat(N),n__isNatKind(N)),N)
r16: plus(N,s(M)) -> U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
r17: |0|() -> n__0()
r18: plus(X1,X2) -> n__plus(X1,X2)
r19: isNatKind(X) -> n__isNatKind(X)
r20: s(X) -> n__s(X)
r21: and(X1,X2) -> n__and(X1,X2)
r22: activate(n__0()) -> |0|()
r23: activate(n__plus(X1,X2)) -> plus(X1,X2)
r24: activate(n__isNatKind(X)) -> isNatKind(X)
r25: activate(n__s(X)) -> s(X)
r26: activate(n__and(X1,X2)) -> and(X1,X2)
r27: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  (no SCCs)

-- Reduction pair.

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

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

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
r2: U12(tt(),V2) -> U13(isNat(activate(V2)))
r3: U13(tt()) -> tt()
r4: U21(tt(),V1) -> U22(isNat(activate(V1)))
r5: U22(tt()) -> tt()
r6: U31(tt(),N) -> activate(N)
r7: U41(tt(),M,N) -> s(plus(activate(N),activate(M)))
r8: and(tt(),X) -> activate(X)
r9: isNat(n__0()) -> tt()
r10: isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))
r11: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r12: isNatKind(n__0()) -> tt()
r13: isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
r14: isNatKind(n__s(V1)) -> isNatKind(activate(V1))
r15: plus(N,|0|()) -> U31(and(isNat(N),n__isNatKind(N)),N)
r16: plus(N,s(M)) -> U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
r17: |0|() -> n__0()
r18: plus(X1,X2) -> n__plus(X1,X2)
r19: isNatKind(X) -> n__isNatKind(X)
r20: s(X) -> n__s(X)
r21: and(X1,X2) -> n__and(X1,X2)
r22: activate(n__0()) -> |0|()
r23: activate(n__plus(X1,X2)) -> plus(X1,X2)
r24: activate(n__isNatKind(X)) -> isNatKind(X)
r25: activate(n__s(X)) -> s(X)
r26: activate(n__and(X1,X2)) -> and(X1,X2)
r27: 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, r19, r20, r21, r22, r23, r24, r25, r26, r27

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          isNatKind#_A(x1) = max{41, x1 + 2}
          n__s_A(x1) = max{38, x1}
          activate_A(x1) = max{35, x1}
          n__plus_A(x1,x2) = max{160, x1 + 14, x2 + 40}
          U13_A(x1) = 56
          tt_A = 55
          U12_A(x1,x2) = max{67, x1 - 142}
          isNat_A(x1) = max{208, x1 + 83}
          U22_A(x1) = max{60, x1 - 126}
          U11_A(x1,x2,x3) = max{161, x1 + 12, x2 + 5}
          U21_A(x1,x2) = max{82, x1 + 6, x2 + 47}
          U31_A(x1,x2) = max{160, x2 + 13}
          U41_A(x1,x2,x3) = max{160, x2 + 40, x3 + 14}
          s_A(x1) = max{38, x1}
          plus_A(x1,x2) = max{160, x1 + 14, x2 + 40}
          n__0_A = 34
          and_A(x1,x2) = max{39, x1 - 21, x2}
          isNatKind_A(x1) = x1 + 77
          n__isNatKind_A(x1) = x1 + 77
          |0|_A = 34
          n__and_A(x1,x2) = max{39, x1 - 21, x2}
    
      precedence:
      
        and = |0| = n__and > activate = U13 = n__0 = isNatKind > n__isNatKind > isNat = U41 = plus > isNatKind# = U12 = U11 > U22 = U21 > tt = s > U31 > n__s > n__plus
      
      partial status:
    
        pi(isNatKind#) = []
        pi(n__s) = []
        pi(activate) = [1]
        pi(n__plus) = [1]
        pi(U13) = []
        pi(tt) = []
        pi(U12) = []
        pi(isNat) = [1]
        pi(U22) = []
        pi(U11) = [2]
        pi(U21) = [1, 2]
        pi(U31) = [2]
        pi(U41) = [3]
        pi(s) = []
        pi(plus) = [1]
        pi(n__0) = []
        pi(and) = [2]
        pi(isNatKind) = []
        pi(n__isNatKind) = [1]
        pi(|0|) = []
        pi(n__and) = [2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          isNatKind#_A(x1) = 121
          n__s_A(x1) = 156
          activate_A(x1) = x1 + 92
          n__plus_A(x1,x2) = x1 + 107
          U13_A(x1) = 1051
          tt_A = 531
          U12_A(x1,x2) = 847
          isNat_A(x1) = 848
          U22_A(x1) = 74
          U11_A(x1,x2,x3) = 848
          U21_A(x1,x2) = max{849, x1 - 376, x2 + 75}
          U31_A(x1,x2) = max{434, x2 + 18}
          U41_A(x1,x2,x3) = 187
          s_A(x1) = 186
          plus_A(x1,x2) = x1 + 187
          n__0_A = 219
          and_A(x1,x2) = max{189, x2 + 98}
          isNatKind_A(x1) = 533
          n__isNatKind_A(x1) = x1 + 442
          |0|_A = 220
          n__and_A(x1,x2) = x2 + 97
    
      precedence:
      
        U13 = tt = plus > U41 > s > n__s > isNatKind# = U22 > activate = n__plus = U31 = and = |0| > U12 = isNat = U11 = U21 = n__0 = isNatKind = n__isNatKind = n__and
      
      partial status:
    
        pi(isNatKind#) = []
        pi(n__s) = []
        pi(activate) = [1]
        pi(n__plus) = [1]
        pi(U13) = []
        pi(tt) = []
        pi(U12) = []
        pi(isNat) = []
        pi(U22) = []
        pi(U11) = []
        pi(U21) = [2]
        pi(U31) = [2]
        pi(U41) = []
        pi(s) = []
        pi(plus) = []
        pi(n__0) = []
        pi(and) = []
        pi(isNatKind) = []
        pi(n__isNatKind) = [1]
        pi(|0|) = []
        pi(n__and) = [2]
    

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
r2: U12(tt(),V2) -> U13(isNat(activate(V2)))
r3: U13(tt()) -> tt()
r4: U21(tt(),V1) -> U22(isNat(activate(V1)))
r5: U22(tt()) -> tt()
r6: U31(tt(),N) -> activate(N)
r7: U41(tt(),M,N) -> s(plus(activate(N),activate(M)))
r8: and(tt(),X) -> activate(X)
r9: isNat(n__0()) -> tt()
r10: isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))
r11: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r12: isNatKind(n__0()) -> tt()
r13: isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
r14: isNatKind(n__s(V1)) -> isNatKind(activate(V1))
r15: plus(N,|0|()) -> U31(and(isNat(N),n__isNatKind(N)),N)
r16: plus(N,s(M)) -> U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
r17: |0|() -> n__0()
r18: plus(X1,X2) -> n__plus(X1,X2)
r19: isNatKind(X) -> n__isNatKind(X)
r20: s(X) -> n__s(X)
r21: and(X1,X2) -> n__and(X1,X2)
r22: activate(n__0()) -> |0|()
r23: activate(n__plus(X1,X2)) -> plus(X1,X2)
r24: activate(n__isNatKind(X)) -> isNatKind(X)
r25: activate(n__s(X)) -> s(X)
r26: activate(n__and(X1,X2)) -> and(X1,X2)
r27: 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: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
r2: U12(tt(),V2) -> U13(isNat(activate(V2)))
r3: U13(tt()) -> tt()
r4: U21(tt(),V1) -> U22(isNat(activate(V1)))
r5: U22(tt()) -> tt()
r6: U31(tt(),N) -> activate(N)
r7: U41(tt(),M,N) -> s(plus(activate(N),activate(M)))
r8: and(tt(),X) -> activate(X)
r9: isNat(n__0()) -> tt()
r10: isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))
r11: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r12: isNatKind(n__0()) -> tt()
r13: isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
r14: isNatKind(n__s(V1)) -> isNatKind(activate(V1))
r15: plus(N,|0|()) -> U31(and(isNat(N),n__isNatKind(N)),N)
r16: plus(N,s(M)) -> U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
r17: |0|() -> n__0()
r18: plus(X1,X2) -> n__plus(X1,X2)
r19: isNatKind(X) -> n__isNatKind(X)
r20: s(X) -> n__s(X)
r21: and(X1,X2) -> n__and(X1,X2)
r22: activate(n__0()) -> |0|()
r23: activate(n__plus(X1,X2)) -> plus(X1,X2)
r24: activate(n__isNatKind(X)) -> isNatKind(X)
r25: activate(n__s(X)) -> s(X)
r26: activate(n__and(X1,X2)) -> and(X1,X2)
r27: 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, r19, r20, r21, r22, r23, r24, r25, r26, r27

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            isNatKind#_A(x1) = ((1,0),(1,1)) x1 + (1,6)
            n__s_A(x1) = x1 + (9,8)
            activate_A(x1) = x1 + (2,1)
            U13_A(x1) = (4,2)
            tt_A() = (3,1)
            U12_A(x1,x2) = ((0,0),(0,1)) x2 + (7,2)
            isNat_A(x1) = x1 + (4,0)
            U22_A(x1) = x1
            U11_A(x1,x2,x3) = x3 + (8,3)
            U21_A(x1,x2) = x2 + (6,7)
            U31_A(x1,x2) = x2 + (3,2)
            U41_A(x1,x2,x3) = ((1,1),(1,1)) x2 + x3 + (28,27)
            s_A(x1) = x1 + (10,8)
            plus_A(x1,x2) = x1 + ((1,1),(1,1)) x2 + (12,15)
            n__0_A() = (0,1)
            n__plus_A(x1,x2) = x1 + ((1,1),(1,1)) x2 + (11,14)
            and_A(x1,x2) = ((0,0),(0,1)) x1 + x2 + (3,0)
            isNatKind_A(x1) = ((1,0),(1,1)) x1 + (4,4)
            n__isNatKind_A(x1) = ((1,0),(1,1)) x1 + (3,4)
            |0|_A() = (0,1)
            n__and_A(x1,x2) = ((0,0),(0,1)) x1 + x2 + (2,0)
    
      precedence:
      
        U11 > U31 > n__s = activate = U13 = tt = U12 = isNat = U22 = U21 = n__0 = and = isNatKind = n__isNatKind = |0| = n__and > plus = n__plus > U41 > s > isNatKind#
      
      partial status:
    
        pi(isNatKind#) = [1]
        pi(n__s) = [1]
        pi(activate) = [1]
        pi(U13) = []
        pi(tt) = []
        pi(U12) = []
        pi(isNat) = []
        pi(U22) = []
        pi(U11) = []
        pi(U21) = []
        pi(U31) = [2]
        pi(U41) = []
        pi(s) = []
        pi(plus) = [2]
        pi(n__0) = []
        pi(n__plus) = [2]
        pi(and) = []
        pi(isNatKind) = []
        pi(n__isNatKind) = []
        pi(|0|) = []
        pi(n__and) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            isNatKind#_A(x1) = ((0,1),(0,1)) x1
            n__s_A(x1) = ((1,1),(1,1)) x1 + (9,3)
            activate_A(x1) = ((1,0),(1,1)) x1 + (4,3)
            U13_A(x1) = (2,1)
            tt_A() = (1,1)
            U12_A(x1,x2) = (8,5)
            isNat_A(x1) = (8,5)
            U22_A(x1) = (2,2)
            U11_A(x1,x2,x3) = (8,5)
            U21_A(x1,x2) = (3,4)
            U31_A(x1,x2) = ((1,0),(1,1)) x2 + (9,3)
            U41_A(x1,x2,x3) = (9,4)
            s_A(x1) = (8,0)
            plus_A(x1,x2) = ((1,0),(0,0)) x2 + (2,5)
            n__0_A() = (8,0)
            n__plus_A(x1,x2) = ((1,0),(0,0)) x2 + (2,5)
            and_A(x1,x2) = (5,2)
            isNatKind_A(x1) = (6,2)
            n__isNatKind_A(x1) = (7,0)
            |0|_A() = (8,0)
            n__and_A(x1,x2) = (4,1)
    
      precedence:
      
        U31 > n__0 = |0| > isNat = U21 > activate = isNatKind > n__and > U11 > and > U12 > U13 > tt = U22 > plus > U41 > n__s = s > isNatKind# > n__plus = n__isNatKind
      
      partial status:
    
        pi(isNatKind#) = []
        pi(n__s) = [1]
        pi(activate) = [1]
        pi(U13) = []
        pi(tt) = []
        pi(U12) = []
        pi(isNat) = []
        pi(U22) = []
        pi(U11) = []
        pi(U21) = []
        pi(U31) = []
        pi(U41) = []
        pi(s) = []
        pi(plus) = []
        pi(n__0) = []
        pi(n__plus) = []
        pi(and) = []
        pi(isNatKind) = []
        pi(n__isNatKind) = []
        pi(|0|) = []
        pi(n__and) = []
    

The next rules are strictly ordered:

  p1

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: plus#(N,s(M)) -> U41#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
p2: U41#(tt(),M,N) -> plus#(activate(N),activate(M))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
r2: U12(tt(),V2) -> U13(isNat(activate(V2)))
r3: U13(tt()) -> tt()
r4: U21(tt(),V1) -> U22(isNat(activate(V1)))
r5: U22(tt()) -> tt()
r6: U31(tt(),N) -> activate(N)
r7: U41(tt(),M,N) -> s(plus(activate(N),activate(M)))
r8: and(tt(),X) -> activate(X)
r9: isNat(n__0()) -> tt()
r10: isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))
r11: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r12: isNatKind(n__0()) -> tt()
r13: isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
r14: isNatKind(n__s(V1)) -> isNatKind(activate(V1))
r15: plus(N,|0|()) -> U31(and(isNat(N),n__isNatKind(N)),N)
r16: plus(N,s(M)) -> U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
r17: |0|() -> n__0()
r18: plus(X1,X2) -> n__plus(X1,X2)
r19: isNatKind(X) -> n__isNatKind(X)
r20: s(X) -> n__s(X)
r21: and(X1,X2) -> n__and(X1,X2)
r22: activate(n__0()) -> |0|()
r23: activate(n__plus(X1,X2)) -> plus(X1,X2)
r24: activate(n__isNatKind(X)) -> isNatKind(X)
r25: activate(n__s(X)) -> s(X)
r26: activate(n__and(X1,X2)) -> and(X1,X2)
r27: 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, r19, r20, r21, r22, r23, r24, r25, r26, r27

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) = x1 + x2 + (38,0)
            s_A(x1) = x1 + (81,8)
            U41#_A(x1,x2,x3) = x2 + x3 + (45,2)
            and_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (4,1)
            isNat_A(x1) = ((1,0),(0,0)) x1 + (25,9)
            n__isNatKind_A(x1) = x1 + (72,1)
            n__and_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (4,1)
            tt_A() = (43,0)
            activate_A(x1) = x1 + (3,1)
            U13_A(x1) = x1 + (1,0)
            U12_A(x1,x2) = ((0,1),(0,0)) x1 + ((1,0),(0,0)) x2 + (30,9)
            U22_A(x1) = (44,0)
            U31_A(x1,x2) = ((1,1),(0,1)) x2 + (70,1)
            U41_A(x1,x2,x3) = ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3 + (141,170)
            plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (52,154)
            U11_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,1),(0,0)) x3 + (43,9)
            U21_A(x1,x2) = (79,0)
            isNatKind_A(x1) = x1 + (74,2)
            n__0_A() = (19,0)
            n__plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (51,153)
            n__s_A(x1) = x1 + (78,8)
            |0|_A() = (19,0)
    
      precedence:
      
        isNat > n__s > isNatKind > and = n__isNatKind > n__and = U11 > plus# = U41# > U12 > U21 > U22 > U13 = n__plus = |0| > U31 = n__0 > s = tt = activate = U41 = plus
      
      partial status:
    
        pi(plus#) = [2]
        pi(s) = []
        pi(U41#) = [2, 3]
        pi(and) = []
        pi(isNat) = []
        pi(n__isNatKind) = []
        pi(n__and) = [2]
        pi(tt) = []
        pi(activate) = []
        pi(U13) = [1]
        pi(U12) = []
        pi(U22) = []
        pi(U31) = [2]
        pi(U41) = []
        pi(plus) = [1]
        pi(U11) = []
        pi(U21) = []
        pi(isNatKind) = []
        pi(n__0) = []
        pi(n__plus) = [1, 2]
        pi(n__s) = []
        pi(|0|) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            plus#_A(x1,x2) = ((0,1),(0,0)) x2
            s_A(x1) = (0,0)
            U41#_A(x1,x2,x3) = ((0,1),(0,0)) x2 + x3 + (6,0)
            and_A(x1,x2) = (5,0)
            isNat_A(x1) = (8,2)
            n__isNatKind_A(x1) = (1,3)
            n__and_A(x1,x2) = ((1,1),(0,0)) x2
            tt_A() = (5,1)
            activate_A(x1) = (5,0)
            U13_A(x1) = ((1,1),(0,1)) x1 + (1,0)
            U12_A(x1,x2) = (12,2)
            U22_A(x1) = (0,0)
            U31_A(x1,x2) = ((1,1),(1,1)) x2 + (4,0)
            U41_A(x1,x2,x3) = (0,0)
            plus_A(x1,x2) = (5,4)
            U11_A(x1,x2,x3) = (13,5)
            U21_A(x1,x2) = (7,1)
            isNatKind_A(x1) = (5,4)
            n__0_A() = (0,0)
            n__plus_A(x1,x2) = ((0,1),(0,1)) x1 + ((0,1),(1,1)) x2 + (5,4)
            n__s_A(x1) = (6,4)
            |0|_A() = (0,0)
    
      precedence:
      
        |0| > n__0 > U41# > isNatKind > U12 > isNat = n__isNatKind = plus > tt > n__s > and = n__and = activate = U31 = n__plus > U13 > U11 > U41 > U21 > plus# = s = U22
      
      partial status:
    
        pi(plus#) = []
        pi(s) = []
        pi(U41#) = [3]
        pi(and) = []
        pi(isNat) = []
        pi(n__isNatKind) = []
        pi(n__and) = []
        pi(tt) = []
        pi(activate) = []
        pi(U13) = [1]
        pi(U12) = []
        pi(U22) = []
        pi(U31) = [2]
        pi(U41) = []
        pi(plus) = []
        pi(U11) = []
        pi(U21) = []
        pi(isNatKind) = []
        pi(n__0) = []
        pi(n__plus) = []
        pi(n__s) = []
        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: U41#(tt(),M,N) -> plus#(activate(N),activate(M))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
r2: U12(tt(),V2) -> U13(isNat(activate(V2)))
r3: U13(tt()) -> tt()
r4: U21(tt(),V1) -> U22(isNat(activate(V1)))
r5: U22(tt()) -> tt()
r6: U31(tt(),N) -> activate(N)
r7: U41(tt(),M,N) -> s(plus(activate(N),activate(M)))
r8: and(tt(),X) -> activate(X)
r9: isNat(n__0()) -> tt()
r10: isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))
r11: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r12: isNatKind(n__0()) -> tt()
r13: isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
r14: isNatKind(n__s(V1)) -> isNatKind(activate(V1))
r15: plus(N,|0|()) -> U31(and(isNat(N),n__isNatKind(N)),N)
r16: plus(N,s(M)) -> U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
r17: |0|() -> n__0()
r18: plus(X1,X2) -> n__plus(X1,X2)
r19: isNatKind(X) -> n__isNatKind(X)
r20: s(X) -> n__s(X)
r21: and(X1,X2) -> n__and(X1,X2)
r22: activate(n__0()) -> |0|()
r23: activate(n__plus(X1,X2)) -> plus(X1,X2)
r24: activate(n__isNatKind(X)) -> isNatKind(X)
r25: activate(n__s(X)) -> s(X)
r26: activate(n__and(X1,X2)) -> and(X1,X2)
r27: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  (no SCCs)