YES

We show the termination of the TRS R:

  U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
  U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
  U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
  U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
  U15(tt(),V2) -> U16(isNat(activate(V2)))
  U16(tt()) -> tt()
  U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
  U22(tt(),V1) -> U23(isNat(activate(V1)))
  U23(tt()) -> tt()
  U31(tt(),V2) -> U32(isNatKind(activate(V2)))
  U32(tt()) -> tt()
  U41(tt()) -> tt()
  U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
  U52(tt(),N) -> activate(N)
  U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
  U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
  U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
  U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
  isNat(n__0()) -> tt()
  isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
  isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
  isNatKind(n__0()) -> tt()
  isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
  isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
  plus(N,|0|()) -> U51(isNat(N),N)
  plus(N,s(M)) -> U61(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(activate(X1),activate(X2))
  activate(n__s(X)) -> s(activate(X))
  activate(X) -> X

-- SCC decomposition.

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

p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2))
p2: U11#(tt(),V1,V2) -> isNatKind#(activate(V1))
p3: U11#(tt(),V1,V2) -> activate#(V1)
p4: U11#(tt(),V1,V2) -> activate#(V2)
p5: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2))
p6: U12#(tt(),V1,V2) -> isNatKind#(activate(V2))
p7: U12#(tt(),V1,V2) -> activate#(V2)
p8: U12#(tt(),V1,V2) -> activate#(V1)
p9: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2))
p10: U13#(tt(),V1,V2) -> isNatKind#(activate(V2))
p11: U13#(tt(),V1,V2) -> activate#(V2)
p12: U13#(tt(),V1,V2) -> activate#(V1)
p13: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2))
p14: U14#(tt(),V1,V2) -> isNat#(activate(V1))
p15: U14#(tt(),V1,V2) -> activate#(V1)
p16: U14#(tt(),V1,V2) -> activate#(V2)
p17: U15#(tt(),V2) -> U16#(isNat(activate(V2)))
p18: U15#(tt(),V2) -> isNat#(activate(V2))
p19: U15#(tt(),V2) -> activate#(V2)
p20: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1))
p21: U21#(tt(),V1) -> isNatKind#(activate(V1))
p22: U21#(tt(),V1) -> activate#(V1)
p23: U22#(tt(),V1) -> U23#(isNat(activate(V1)))
p24: U22#(tt(),V1) -> isNat#(activate(V1))
p25: U22#(tt(),V1) -> activate#(V1)
p26: U31#(tt(),V2) -> U32#(isNatKind(activate(V2)))
p27: U31#(tt(),V2) -> isNatKind#(activate(V2))
p28: U31#(tt(),V2) -> activate#(V2)
p29: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N))
p30: U51#(tt(),N) -> isNatKind#(activate(N))
p31: U51#(tt(),N) -> activate#(N)
p32: U52#(tt(),N) -> activate#(N)
p33: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N))
p34: U61#(tt(),M,N) -> isNatKind#(activate(M))
p35: U61#(tt(),M,N) -> activate#(M)
p36: U61#(tt(),M,N) -> activate#(N)
p37: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N))
p38: U62#(tt(),M,N) -> isNat#(activate(N))
p39: U62#(tt(),M,N) -> activate#(N)
p40: U62#(tt(),M,N) -> activate#(M)
p41: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N))
p42: U63#(tt(),M,N) -> isNatKind#(activate(N))
p43: U63#(tt(),M,N) -> activate#(N)
p44: U63#(tt(),M,N) -> activate#(M)
p45: U64#(tt(),M,N) -> s#(plus(activate(N),activate(M)))
p46: U64#(tt(),M,N) -> plus#(activate(N),activate(M))
p47: U64#(tt(),M,N) -> activate#(N)
p48: U64#(tt(),M,N) -> activate#(M)
p49: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2))
p50: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p51: isNat#(n__plus(V1,V2)) -> activate#(V1)
p52: isNat#(n__plus(V1,V2)) -> activate#(V2)
p53: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p54: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p55: isNat#(n__s(V1)) -> activate#(V1)
p56: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2))
p57: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p58: isNatKind#(n__plus(V1,V2)) -> activate#(V1)
p59: isNatKind#(n__plus(V1,V2)) -> activate#(V2)
p60: isNatKind#(n__s(V1)) -> U41#(isNatKind(activate(V1)))
p61: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
p62: isNatKind#(n__s(V1)) -> activate#(V1)
p63: plus#(N,|0|()) -> U51#(isNat(N),N)
p64: plus#(N,|0|()) -> isNat#(N)
p65: plus#(N,s(M)) -> U61#(isNat(M),M,N)
p66: plus#(N,s(M)) -> isNat#(M)
p67: activate#(n__0()) -> |0|#()
p68: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2))
p69: activate#(n__plus(X1,X2)) -> activate#(X1)
p70: activate#(n__plus(X1,X2)) -> activate#(X2)
p71: activate#(n__s(X)) -> s#(activate(X))
p72: activate#(n__s(X)) -> activate#(X)

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p18, p19, p20, p21, p22, p24, p25, p27, p28, p29, p30, p31, p32, p33, p34, p35, p36, p37, p38, p39, p40, p41, p42, p43, p44, p46, p47, p48, p49, p50, p51, p52, p53, p54, p55, p56, p57, p58, p59, p61, p62, p63, p64, p65, p66, p68, p69, p70, p72}


-- Reduction pair.

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

p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2))
p2: U12#(tt(),V1,V2) -> activate#(V1)
p3: activate#(n__s(X)) -> activate#(X)
p4: activate#(n__plus(X1,X2)) -> activate#(X2)
p5: activate#(n__plus(X1,X2)) -> activate#(X1)
p6: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2))
p7: plus#(N,s(M)) -> isNat#(M)
p8: isNat#(n__s(V1)) -> activate#(V1)
p9: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p10: isNatKind#(n__s(V1)) -> 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)) -> U31#(isNatKind(activate(V1)),activate(V2))
p16: U31#(tt(),V2) -> activate#(V2)
p17: U31#(tt(),V2) -> isNatKind#(activate(V2))
p18: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p19: U21#(tt(),V1) -> activate#(V1)
p20: U21#(tt(),V1) -> isNatKind#(activate(V1))
p21: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1))
p22: U22#(tt(),V1) -> activate#(V1)
p23: U22#(tt(),V1) -> isNat#(activate(V1))
p24: isNat#(n__plus(V1,V2)) -> activate#(V2)
p25: isNat#(n__plus(V1,V2)) -> activate#(V1)
p26: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p27: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2))
p28: U11#(tt(),V1,V2) -> activate#(V2)
p29: U11#(tt(),V1,V2) -> activate#(V1)
p30: U11#(tt(),V1,V2) -> isNatKind#(activate(V1))
p31: plus#(N,s(M)) -> U61#(isNat(M),M,N)
p32: U61#(tt(),M,N) -> activate#(N)
p33: U61#(tt(),M,N) -> activate#(M)
p34: U61#(tt(),M,N) -> isNatKind#(activate(M))
p35: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N))
p36: U62#(tt(),M,N) -> activate#(M)
p37: U62#(tt(),M,N) -> activate#(N)
p38: U62#(tt(),M,N) -> isNat#(activate(N))
p39: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N))
p40: U63#(tt(),M,N) -> activate#(M)
p41: U63#(tt(),M,N) -> activate#(N)
p42: U63#(tt(),M,N) -> isNatKind#(activate(N))
p43: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N))
p44: U64#(tt(),M,N) -> activate#(M)
p45: U64#(tt(),M,N) -> activate#(N)
p46: U64#(tt(),M,N) -> plus#(activate(N),activate(M))
p47: plus#(N,|0|()) -> isNat#(N)
p48: plus#(N,|0|()) -> U51#(isNat(N),N)
p49: U51#(tt(),N) -> activate#(N)
p50: U51#(tt(),N) -> isNatKind#(activate(N))
p51: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N))
p52: U52#(tt(),N) -> activate#(N)
p53: U12#(tt(),V1,V2) -> activate#(V2)
p54: U12#(tt(),V1,V2) -> isNatKind#(activate(V2))
p55: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2))
p56: U13#(tt(),V1,V2) -> activate#(V1)
p57: U13#(tt(),V1,V2) -> activate#(V2)
p58: U13#(tt(),V1,V2) -> isNatKind#(activate(V2))
p59: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2))
p60: U14#(tt(),V1,V2) -> activate#(V2)
p61: U14#(tt(),V1,V2) -> activate#(V1)
p62: U14#(tt(),V1,V2) -> isNat#(activate(V1))
p63: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2))
p64: U15#(tt(),V2) -> activate#(V2)
p65: U15#(tt(),V2) -> isNat#(activate(V2))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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, r28, r29, r30, r31, r32, r33

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          U11#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,1)) x3 + (20,25)
          tt_A() = (11,0)
          U12#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (19,9)
          isNatKind_A(x1) = ((1,0),(0,0)) x1 + (2,48)
          activate_A(x1) = ((1,0),(1,1)) x1 + (0,15)
          activate#_A(x1) = ((1,0),(0,0)) x1 + (13,7)
          n__s_A(x1) = ((1,0),(1,0)) x1 + (14,1)
          n__plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (14,41)
          plus#_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (12,4)
          s_A(x1) = ((1,0),(1,0)) x1 + (14,2)
          isNat#_A(x1) = x1 + (12,6)
          isNatKind#_A(x1) = ((1,0),(0,0)) x1 + (17,3)
          U31#_A(x1,x2) = ((1,0),(0,0)) x2 + (17,3)
          U21#_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (17,38)
          U22#_A(x1,x2) = x2 + (13,22)
          U61#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (18,5)
          isNat_A(x1) = ((0,0),(1,0)) x1 + (16,0)
          U62#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (17,5)
          U63#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (17,4)
          U64#_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (14,1)
          |0|_A() = (10,1)
          U51#_A(x1,x2) = ((1,0),(0,0)) x2 + (17,5)
          U52#_A(x1,x2) = ((1,0),(0,0)) x2 + (14,8)
          U13#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (18,8)
          U14#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (15,23)
          U15#_A(x1,x2) = ((1,0),(0,0)) x2 + (14,22)
          U16_A(x1) = ((0,0),(1,0)) x1 + (12,1)
          U15_A(x1,x2) = (13,18)
          U64_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (28,17)
          plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (14,70)
          U14_A(x1,x2,x3) = ((0,0),(1,0)) x2 + (14,19)
          U63_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (28,18)
          U13_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (15,9)
          U23_A(x1) = ((1,0),(0,0)) x1 + (0,14)
          U52_A(x1,x2) = ((1,0),(1,1)) x2 + (0,16)
          U62_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (28,19)
          U12_A(x1,x2,x3) = (16,12)
          U22_A(x1,x2) = ((0,0),(1,0)) x2 + (16,14)
          U32_A(x1) = (11,0)
          U51_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (1,2)
          U61_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (28,49)
          U11_A(x1,x2,x3) = (16,13)
          U21_A(x1,x2) = ((0,0),(1,0)) x2 + (16,14)
          U31_A(x1,x2) = ((1,0),(0,0)) x1 + (0,42)
          U41_A(x1) = ((1,0),(0,0)) x1 + (0,2)
          n__0_A() = (10,1)
  
    precedence:
    
      U21# = U61# > U22# > |0| = n__0 > isNat# > U11# = U12# = isNatKind# = U31# = isNat = U63# = U13# = U21 > U64# > U14# > activate# = U52# = U15# > U62# > U51# = U52 = U11 > U13 = U12 > U14 > U15 > activate > n__plus = plus = U61 > U62 > tt = isNatKind = U16 = U23 = U22 = U32 = U31 = U41 > plus# > U51 > U63 > U64 > s > n__s
    
    partial status:
  
      pi(U11#) = []
      pi(tt) = []
      pi(U12#) = []
      pi(isNatKind) = []
      pi(activate) = [1]
      pi(activate#) = []
      pi(n__s) = []
      pi(n__plus) = []
      pi(plus#) = [2]
      pi(s) = []
      pi(isNat#) = [1]
      pi(isNatKind#) = []
      pi(U31#) = []
      pi(U21#) = []
      pi(U22#) = [2]
      pi(U61#) = []
      pi(isNat) = []
      pi(U62#) = []
      pi(U63#) = []
      pi(U64#) = []
      pi(|0|) = []
      pi(U51#) = []
      pi(U52#) = []
      pi(U13#) = []
      pi(U14#) = []
      pi(U15#) = []
      pi(U16) = []
      pi(U15) = []
      pi(U64) = []
      pi(plus) = []
      pi(U14) = []
      pi(U63) = []
      pi(U13) = []
      pi(U23) = []
      pi(U52) = []
      pi(U62) = []
      pi(U12) = []
      pi(U22) = []
      pi(U32) = []
      pi(U51) = []
      pi(U61) = []
      pi(U11) = []
      pi(U21) = []
      pi(U31) = []
      pi(U41) = []
      pi(n__0) = []

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: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2))
p2: activate#(n__s(X)) -> activate#(X)
p3: activate#(n__plus(X1,X2)) -> activate#(X2)
p4: activate#(n__plus(X1,X2)) -> activate#(X1)
p5: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2))
p6: plus#(N,s(M)) -> isNat#(M)
p7: isNat#(n__s(V1)) -> activate#(V1)
p8: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p9: isNatKind#(n__s(V1)) -> activate#(V1)
p10: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
p11: isNatKind#(n__plus(V1,V2)) -> activate#(V2)
p12: isNatKind#(n__plus(V1,V2)) -> activate#(V1)
p13: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p14: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2))
p15: U31#(tt(),V2) -> activate#(V2)
p16: U31#(tt(),V2) -> isNatKind#(activate(V2))
p17: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p18: U21#(tt(),V1) -> activate#(V1)
p19: U21#(tt(),V1) -> isNatKind#(activate(V1))
p20: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1))
p21: U22#(tt(),V1) -> activate#(V1)
p22: U22#(tt(),V1) -> isNat#(activate(V1))
p23: isNat#(n__plus(V1,V2)) -> activate#(V2)
p24: isNat#(n__plus(V1,V2)) -> activate#(V1)
p25: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p26: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2))
p27: U11#(tt(),V1,V2) -> activate#(V2)
p28: U11#(tt(),V1,V2) -> activate#(V1)
p29: U11#(tt(),V1,V2) -> isNatKind#(activate(V1))
p30: plus#(N,s(M)) -> U61#(isNat(M),M,N)
p31: U61#(tt(),M,N) -> activate#(N)
p32: U61#(tt(),M,N) -> activate#(M)
p33: U61#(tt(),M,N) -> isNatKind#(activate(M))
p34: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N))
p35: U62#(tt(),M,N) -> activate#(M)
p36: U62#(tt(),M,N) -> activate#(N)
p37: U62#(tt(),M,N) -> isNat#(activate(N))
p38: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N))
p39: U63#(tt(),M,N) -> activate#(M)
p40: U63#(tt(),M,N) -> activate#(N)
p41: U63#(tt(),M,N) -> isNatKind#(activate(N))
p42: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N))
p43: U64#(tt(),M,N) -> activate#(M)
p44: U64#(tt(),M,N) -> activate#(N)
p45: U64#(tt(),M,N) -> plus#(activate(N),activate(M))
p46: plus#(N,|0|()) -> isNat#(N)
p47: plus#(N,|0|()) -> U51#(isNat(N),N)
p48: U51#(tt(),N) -> activate#(N)
p49: U51#(tt(),N) -> isNatKind#(activate(N))
p50: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N))
p51: U52#(tt(),N) -> activate#(N)
p52: U12#(tt(),V1,V2) -> activate#(V2)
p53: U12#(tt(),V1,V2) -> isNatKind#(activate(V2))
p54: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2))
p55: U13#(tt(),V1,V2) -> activate#(V1)
p56: U13#(tt(),V1,V2) -> activate#(V2)
p57: U13#(tt(),V1,V2) -> isNatKind#(activate(V2))
p58: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2))
p59: U14#(tt(),V1,V2) -> activate#(V2)
p60: U14#(tt(),V1,V2) -> activate#(V1)
p61: U14#(tt(),V1,V2) -> isNat#(activate(V1))
p62: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2))
p63: U15#(tt(),V2) -> activate#(V2)
p64: U15#(tt(),V2) -> isNat#(activate(V2))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: activate(X) -> X

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, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32, p33, p34, p35, p36, p37, p38, p39, p40, p41, p42, p43, p44, p45, p46, p47, p48, p49, p50, p51, p52, p53, p54, p55, p56, p57, p58, p59, p60, p61, p62, p63, p64}


-- Reduction pair.

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

p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2))
p2: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2))
p3: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2))
p4: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2))
p5: U15#(tt(),V2) -> isNat#(activate(V2))
p6: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2))
p7: U11#(tt(),V1,V2) -> isNatKind#(activate(V1))
p8: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2))
p9: U31#(tt(),V2) -> isNatKind#(activate(V2))
p10: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p11: isNatKind#(n__plus(V1,V2)) -> activate#(V1)
p12: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2))
p13: plus#(N,|0|()) -> U51#(isNat(N),N)
p14: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N))
p15: U52#(tt(),N) -> activate#(N)
p16: activate#(n__plus(X1,X2)) -> activate#(X1)
p17: activate#(n__plus(X1,X2)) -> activate#(X2)
p18: activate#(n__s(X)) -> activate#(X)
p19: U51#(tt(),N) -> isNatKind#(activate(N))
p20: isNatKind#(n__plus(V1,V2)) -> activate#(V2)
p21: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
p22: isNatKind#(n__s(V1)) -> activate#(V1)
p23: U51#(tt(),N) -> activate#(N)
p24: plus#(N,|0|()) -> isNat#(N)
p25: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p26: isNat#(n__plus(V1,V2)) -> activate#(V1)
p27: isNat#(n__plus(V1,V2)) -> activate#(V2)
p28: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p29: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1))
p30: U22#(tt(),V1) -> isNat#(activate(V1))
p31: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p32: isNat#(n__s(V1)) -> activate#(V1)
p33: U22#(tt(),V1) -> activate#(V1)
p34: U21#(tt(),V1) -> isNatKind#(activate(V1))
p35: U21#(tt(),V1) -> activate#(V1)
p36: plus#(N,s(M)) -> U61#(isNat(M),M,N)
p37: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N))
p38: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N))
p39: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N))
p40: U64#(tt(),M,N) -> plus#(activate(N),activate(M))
p41: plus#(N,s(M)) -> isNat#(M)
p42: U64#(tt(),M,N) -> activate#(N)
p43: U64#(tt(),M,N) -> activate#(M)
p44: U63#(tt(),M,N) -> isNatKind#(activate(N))
p45: U63#(tt(),M,N) -> activate#(N)
p46: U63#(tt(),M,N) -> activate#(M)
p47: U62#(tt(),M,N) -> isNat#(activate(N))
p48: U62#(tt(),M,N) -> activate#(N)
p49: U62#(tt(),M,N) -> activate#(M)
p50: U61#(tt(),M,N) -> isNatKind#(activate(M))
p51: U61#(tt(),M,N) -> activate#(M)
p52: U61#(tt(),M,N) -> activate#(N)
p53: U31#(tt(),V2) -> activate#(V2)
p54: U11#(tt(),V1,V2) -> activate#(V1)
p55: U11#(tt(),V1,V2) -> activate#(V2)
p56: U15#(tt(),V2) -> activate#(V2)
p57: U14#(tt(),V1,V2) -> isNat#(activate(V1))
p58: U14#(tt(),V1,V2) -> activate#(V1)
p59: U14#(tt(),V1,V2) -> activate#(V2)
p60: U13#(tt(),V1,V2) -> isNatKind#(activate(V2))
p61: U13#(tt(),V1,V2) -> activate#(V2)
p62: U13#(tt(),V1,V2) -> activate#(V1)
p63: U12#(tt(),V1,V2) -> isNatKind#(activate(V2))
p64: U12#(tt(),V1,V2) -> activate#(V2)

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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, r28, r29, r30, r31, r32, r33

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          U11#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (15,143)
          tt_A() = (10,61)
          U12#_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (14,126)
          isNatKind_A(x1) = ((0,0),(1,0)) x1 + (16,98)
          activate_A(x1) = x1 + (0,18)
          U13#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + x3 + (13,136)
          U14#_A(x1,x2,x3) = x2 + ((1,0),(0,0)) x3 + (12,76)
          U15#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (3,57)
          isNat_A(x1) = x1 + (6,148)
          isNat#_A(x1) = x1 + (11,20)
          n__plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (19,35)
          isNatKind#_A(x1) = ((1,0),(0,0)) x1 + (11,135)
          U31#_A(x1,x2) = ((1,0),(0,0)) x2 + (30,135)
          activate#_A(x1) = ((1,0),(0,0)) x1 + (12,56)
          plus#_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (11,24)
          |0|_A() = (95,17)
          U51#_A(x1,x2) = x2 + (106,135)
          U52#_A(x1,x2) = x2 + (13,117)
          n__s_A(x1) = ((1,0),(0,0)) x1 + (13,18)
          U21#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (7,38)
          U22#_A(x1,x2) = ((1,0),(0,0)) x2 + (17,38)
          s_A(x1) = ((1,0),(0,0)) x1 + (13,19)
          U61#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (24,56)
          U62#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (24,38)
          U63#_A(x1,x2,x3) = x2 + x3 + (19,135)
          U64#_A(x1,x2,x3) = x1 + ((1,0),(1,1)) x2 + ((1,0),(1,1)) x3 + (2,1)
          U16_A(x1) = (11,62)
          U15_A(x1,x2) = (12,63)
          U64_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (32,62)
          plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (19,52)
          U14_A(x1,x2,x3) = (13,64)
          U63_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (32,62)
          U13_A(x1,x2,x3) = ((0,0),(1,0)) x1 + (16,55)
          U23_A(x1) = ((0,0),(1,0)) x1 + (10,56)
          U52_A(x1,x2) = ((1,0),(0,0)) x2 + (11,17)
          U62_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (32,63)
          U12_A(x1,x2,x3) = ((0,0),(1,0)) x1 + x3 + (17,62)
          U22_A(x1,x2) = ((0,0),(1,0)) x1 + (11,46)
          U32_A(x1) = (14,62)
          U51_A(x1,x2) = x2 + (15,148)
          U61_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (32,64)
          U11_A(x1,x2,x3) = ((0,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (18,97)
          U21_A(x1,x2) = ((0,0),(1,0)) x1 + (12,1)
          U31_A(x1,x2) = (15,118)
          U41_A(x1) = (14,17)
          n__0_A() = (95,0)
  
    precedence:
    
      U52 > U22 = U21 > U13# = U14# = U23 = U41 > activate = U15# = |0| > s = n__0 > activate# = U51# = U52# = U63# = U64# > plus# > U11# = isNatKind = isNat = isNat# = U21# = U22# > U12# > isNatKind# = U31# = U61# = U62# > tt = n__plus = U16 = U15 = plus = U32 = U51 = U61 = U31 > n__s > U13 = U12 = U11 > U64 = U14 = U63 = U62
    
    partial status:
  
      pi(U11#) = []
      pi(tt) = []
      pi(U12#) = []
      pi(isNatKind) = []
      pi(activate) = []
      pi(U13#) = [2]
      pi(U14#) = []
      pi(U15#) = []
      pi(isNat) = []
      pi(isNat#) = []
      pi(n__plus) = []
      pi(isNatKind#) = []
      pi(U31#) = []
      pi(activate#) = []
      pi(plus#) = [1]
      pi(|0|) = []
      pi(U51#) = []
      pi(U52#) = []
      pi(n__s) = []
      pi(U21#) = []
      pi(U22#) = []
      pi(s) = []
      pi(U61#) = []
      pi(U62#) = []
      pi(U63#) = [3]
      pi(U64#) = []
      pi(U16) = []
      pi(U15) = []
      pi(U64) = []
      pi(plus) = []
      pi(U14) = []
      pi(U63) = []
      pi(U13) = []
      pi(U23) = []
      pi(U52) = []
      pi(U62) = []
      pi(U12) = []
      pi(U22) = []
      pi(U32) = []
      pi(U51) = []
      pi(U61) = []
      pi(U11) = []
      pi(U21) = []
      pi(U31) = []
      pi(U41) = []
      pi(n__0) = []

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: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2))
p2: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2))
p3: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2))
p4: U15#(tt(),V2) -> isNat#(activate(V2))
p5: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2))
p6: U11#(tt(),V1,V2) -> isNatKind#(activate(V1))
p7: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2))
p8: U31#(tt(),V2) -> isNatKind#(activate(V2))
p9: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p10: isNatKind#(n__plus(V1,V2)) -> activate#(V1)
p11: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2))
p12: plus#(N,|0|()) -> U51#(isNat(N),N)
p13: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N))
p14: U52#(tt(),N) -> activate#(N)
p15: activate#(n__plus(X1,X2)) -> activate#(X1)
p16: activate#(n__plus(X1,X2)) -> activate#(X2)
p17: activate#(n__s(X)) -> activate#(X)
p18: U51#(tt(),N) -> isNatKind#(activate(N))
p19: isNatKind#(n__plus(V1,V2)) -> activate#(V2)
p20: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
p21: isNatKind#(n__s(V1)) -> activate#(V1)
p22: U51#(tt(),N) -> activate#(N)
p23: plus#(N,|0|()) -> isNat#(N)
p24: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p25: isNat#(n__plus(V1,V2)) -> activate#(V1)
p26: isNat#(n__plus(V1,V2)) -> activate#(V2)
p27: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p28: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1))
p29: U22#(tt(),V1) -> isNat#(activate(V1))
p30: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p31: isNat#(n__s(V1)) -> activate#(V1)
p32: U22#(tt(),V1) -> activate#(V1)
p33: U21#(tt(),V1) -> isNatKind#(activate(V1))
p34: U21#(tt(),V1) -> activate#(V1)
p35: plus#(N,s(M)) -> U61#(isNat(M),M,N)
p36: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N))
p37: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N))
p38: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N))
p39: U64#(tt(),M,N) -> plus#(activate(N),activate(M))
p40: plus#(N,s(M)) -> isNat#(M)
p41: U64#(tt(),M,N) -> activate#(N)
p42: U64#(tt(),M,N) -> activate#(M)
p43: U63#(tt(),M,N) -> isNatKind#(activate(N))
p44: U63#(tt(),M,N) -> activate#(N)
p45: U63#(tt(),M,N) -> activate#(M)
p46: U62#(tt(),M,N) -> isNat#(activate(N))
p47: U62#(tt(),M,N) -> activate#(N)
p48: U62#(tt(),M,N) -> activate#(M)
p49: U61#(tt(),M,N) -> isNatKind#(activate(M))
p50: U61#(tt(),M,N) -> activate#(M)
p51: U61#(tt(),M,N) -> activate#(N)
p52: U31#(tt(),V2) -> activate#(V2)
p53: U11#(tt(),V1,V2) -> activate#(V1)
p54: U11#(tt(),V1,V2) -> activate#(V2)
p55: U15#(tt(),V2) -> activate#(V2)
p56: U14#(tt(),V1,V2) -> isNat#(activate(V1))
p57: U14#(tt(),V1,V2) -> activate#(V1)
p58: U14#(tt(),V1,V2) -> activate#(V2)
p59: U13#(tt(),V1,V2) -> isNatKind#(activate(V2))
p60: U13#(tt(),V1,V2) -> activate#(V2)
p61: U13#(tt(),V1,V2) -> activate#(V1)
p62: U12#(tt(),V1,V2) -> isNatKind#(activate(V2))
p63: U12#(tt(),V1,V2) -> activate#(V2)

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p5, p6, p7, p8, p9, p10, p11, p12, 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, p39, p40, p41, p42, p43, p44, p45, p46, p47, p48, p49, p50, p51, p52, p53, p54, p62, p63}


-- Reduction pair.

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

p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2))
p2: U12#(tt(),V1,V2) -> activate#(V2)
p3: activate#(n__s(X)) -> activate#(X)
p4: activate#(n__plus(X1,X2)) -> activate#(X2)
p5: activate#(n__plus(X1,X2)) -> activate#(X1)
p6: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2))
p7: plus#(N,s(M)) -> isNat#(M)
p8: isNat#(n__s(V1)) -> activate#(V1)
p9: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p10: isNatKind#(n__s(V1)) -> 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)) -> U31#(isNatKind(activate(V1)),activate(V2))
p16: U31#(tt(),V2) -> activate#(V2)
p17: U31#(tt(),V2) -> isNatKind#(activate(V2))
p18: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p19: U21#(tt(),V1) -> activate#(V1)
p20: U21#(tt(),V1) -> isNatKind#(activate(V1))
p21: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1))
p22: U22#(tt(),V1) -> activate#(V1)
p23: U22#(tt(),V1) -> isNat#(activate(V1))
p24: isNat#(n__plus(V1,V2)) -> activate#(V2)
p25: isNat#(n__plus(V1,V2)) -> activate#(V1)
p26: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p27: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2))
p28: U11#(tt(),V1,V2) -> activate#(V2)
p29: U11#(tt(),V1,V2) -> activate#(V1)
p30: U11#(tt(),V1,V2) -> isNatKind#(activate(V1))
p31: plus#(N,s(M)) -> U61#(isNat(M),M,N)
p32: U61#(tt(),M,N) -> activate#(N)
p33: U61#(tt(),M,N) -> activate#(M)
p34: U61#(tt(),M,N) -> isNatKind#(activate(M))
p35: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N))
p36: U62#(tt(),M,N) -> activate#(M)
p37: U62#(tt(),M,N) -> activate#(N)
p38: U62#(tt(),M,N) -> isNat#(activate(N))
p39: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N))
p40: U63#(tt(),M,N) -> activate#(M)
p41: U63#(tt(),M,N) -> activate#(N)
p42: U63#(tt(),M,N) -> isNatKind#(activate(N))
p43: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N))
p44: U64#(tt(),M,N) -> activate#(M)
p45: U64#(tt(),M,N) -> activate#(N)
p46: U64#(tt(),M,N) -> plus#(activate(N),activate(M))
p47: plus#(N,|0|()) -> isNat#(N)
p48: plus#(N,|0|()) -> U51#(isNat(N),N)
p49: U51#(tt(),N) -> activate#(N)
p50: U51#(tt(),N) -> isNatKind#(activate(N))
p51: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N))
p52: U52#(tt(),N) -> activate#(N)
p53: U12#(tt(),V1,V2) -> isNatKind#(activate(V2))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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, r28, r29, r30, r31, r32, r33

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          U11#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,1)) x3 + (11,31)
          tt_A() = (18,0)
          U12#_A(x1,x2,x3) = ((0,0),(1,0)) x2 + x3 + (10,54)
          isNatKind_A(x1) = ((1,0),(1,0)) x1 + (8,20)
          activate_A(x1) = x1 + (0,22)
          activate#_A(x1) = ((1,0),(0,0)) x1 + (3,53)
          n__s_A(x1) = ((1,0),(0,0)) x1 + (15,18)
          n__plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (0,10)
          plus#_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (2,42)
          s_A(x1) = ((1,0),(0,0)) x1 + (15,40)
          isNat#_A(x1) = x1 + (12,42)
          isNatKind#_A(x1) = ((1,0),(0,0)) x1 + (9,21)
          U31#_A(x1,x2) = ((1,0),(0,0)) x2 + (9,21)
          U21#_A(x1,x2) = ((1,0),(0,0)) x2 + (14,59)
          U22#_A(x1,x2) = ((1,0),(0,0)) x2 + (13,58)
          U61#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (16,41)
          isNat_A(x1) = ((1,0),(0,0)) x1 + (18,0)
          U62#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (15,89)
          U63#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,1)) x3 + (14,66)
          U64#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (13,65)
          |0|_A() = (10,1)
          U51#_A(x1,x2) = ((1,0),(1,0)) x2 + (11,23)
          U52#_A(x1,x2) = ((1,0),(0,0)) x2 + (11,23)
          U16_A(x1) = (19,1)
          U15_A(x1,x2) = ((1,0),(0,0)) x1 + (2,2)
          U64_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (15,42)
          plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (0,31)
          U14_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (3,3)
          U63_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (15,43)
          U13_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (12,4)
          U23_A(x1) = (19,2)
          U52_A(x1,x2) = ((1,0),(0,0)) x2 + (6,1)
          U62_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (15,44)
          U12_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + x3 + (13,1)
          U22_A(x1,x2) = (20,1)
          U32_A(x1) = ((1,0),(0,0)) x1 + (1,1)
          U51_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (7,1)
          U61_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (15,45)
          U11_A(x1,x2,x3) = ((1,0),(1,1)) x2 + x3 + (14,32)
          U21_A(x1,x2) = (21,19)
          U31_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (0,3)
          U41_A(x1) = (19,36)
          n__0_A() = (10,1)
  
    precedence:
    
      U11# = tt = U12# = isNatKind = activate = activate# = n__s = n__plus = plus# = s = isNat# = isNatKind# = U31# = U21# = U22# = U61# = isNat = U62# = U63# = U64# = U51# = U52# = U16 = U15 = U64 = plus = U14 = U63 = U13 = U23 = U52 = U62 = U12 = U22 = U32 = U51 = U61 = U11 = U21 = U31 = U41 > |0| = n__0
    
    partial status:
  
      pi(U11#) = []
      pi(tt) = []
      pi(U12#) = []
      pi(isNatKind) = []
      pi(activate) = []
      pi(activate#) = []
      pi(n__s) = []
      pi(n__plus) = []
      pi(plus#) = []
      pi(s) = []
      pi(isNat#) = []
      pi(isNatKind#) = []
      pi(U31#) = []
      pi(U21#) = []
      pi(U22#) = []
      pi(U61#) = []
      pi(isNat) = []
      pi(U62#) = []
      pi(U63#) = []
      pi(U64#) = []
      pi(|0|) = []
      pi(U51#) = []
      pi(U52#) = []
      pi(U16) = []
      pi(U15) = []
      pi(U64) = []
      pi(plus) = []
      pi(U14) = []
      pi(U63) = []
      pi(U13) = []
      pi(U23) = []
      pi(U52) = []
      pi(U62) = []
      pi(U12) = []
      pi(U22) = []
      pi(U32) = []
      pi(U51) = []
      pi(U61) = []
      pi(U11) = []
      pi(U21) = []
      pi(U31) = []
      pi(U41) = []
      pi(n__0) = []

The next rules are strictly ordered:

  p20

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#(isNatKind(activate(V1)),activate(V1),activate(V2))
p2: U12#(tt(),V1,V2) -> activate#(V2)
p3: activate#(n__s(X)) -> activate#(X)
p4: activate#(n__plus(X1,X2)) -> activate#(X2)
p5: activate#(n__plus(X1,X2)) -> activate#(X1)
p6: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2))
p7: plus#(N,s(M)) -> isNat#(M)
p8: isNat#(n__s(V1)) -> activate#(V1)
p9: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p10: isNatKind#(n__s(V1)) -> 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)) -> U31#(isNatKind(activate(V1)),activate(V2))
p16: U31#(tt(),V2) -> activate#(V2)
p17: U31#(tt(),V2) -> isNatKind#(activate(V2))
p18: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p19: U21#(tt(),V1) -> activate#(V1)
p20: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1))
p21: U22#(tt(),V1) -> activate#(V1)
p22: U22#(tt(),V1) -> isNat#(activate(V1))
p23: isNat#(n__plus(V1,V2)) -> activate#(V2)
p24: isNat#(n__plus(V1,V2)) -> activate#(V1)
p25: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p26: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2))
p27: U11#(tt(),V1,V2) -> activate#(V2)
p28: U11#(tt(),V1,V2) -> activate#(V1)
p29: U11#(tt(),V1,V2) -> isNatKind#(activate(V1))
p30: plus#(N,s(M)) -> U61#(isNat(M),M,N)
p31: U61#(tt(),M,N) -> activate#(N)
p32: U61#(tt(),M,N) -> activate#(M)
p33: U61#(tt(),M,N) -> isNatKind#(activate(M))
p34: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N))
p35: U62#(tt(),M,N) -> activate#(M)
p36: U62#(tt(),M,N) -> activate#(N)
p37: U62#(tt(),M,N) -> isNat#(activate(N))
p38: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N))
p39: U63#(tt(),M,N) -> activate#(M)
p40: U63#(tt(),M,N) -> activate#(N)
p41: U63#(tt(),M,N) -> isNatKind#(activate(N))
p42: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N))
p43: U64#(tt(),M,N) -> activate#(M)
p44: U64#(tt(),M,N) -> activate#(N)
p45: U64#(tt(),M,N) -> plus#(activate(N),activate(M))
p46: plus#(N,|0|()) -> isNat#(N)
p47: plus#(N,|0|()) -> U51#(isNat(N),N)
p48: U51#(tt(),N) -> activate#(N)
p49: U51#(tt(),N) -> isNatKind#(activate(N))
p50: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N))
p51: U52#(tt(),N) -> activate#(N)
p52: U12#(tt(),V1,V2) -> isNatKind#(activate(V2))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: activate(X) -> X

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, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32, p33, p34, p35, p36, p37, p38, p39, p40, p41, p42, p43, p44, p45, p46, p47, p48, p49, p50, p51, p52}


-- Reduction pair.

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

p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2))
p2: U12#(tt(),V1,V2) -> isNatKind#(activate(V2))
p3: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2))
p4: U31#(tt(),V2) -> isNatKind#(activate(V2))
p5: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p6: isNatKind#(n__plus(V1,V2)) -> activate#(V1)
p7: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2))
p8: plus#(N,|0|()) -> U51#(isNat(N),N)
p9: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N))
p10: U52#(tt(),N) -> activate#(N)
p11: activate#(n__plus(X1,X2)) -> activate#(X1)
p12: activate#(n__plus(X1,X2)) -> activate#(X2)
p13: activate#(n__s(X)) -> activate#(X)
p14: U51#(tt(),N) -> isNatKind#(activate(N))
p15: isNatKind#(n__plus(V1,V2)) -> activate#(V2)
p16: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
p17: isNatKind#(n__s(V1)) -> activate#(V1)
p18: U51#(tt(),N) -> activate#(N)
p19: plus#(N,|0|()) -> isNat#(N)
p20: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2))
p21: U11#(tt(),V1,V2) -> isNatKind#(activate(V1))
p22: U11#(tt(),V1,V2) -> activate#(V1)
p23: U11#(tt(),V1,V2) -> activate#(V2)
p24: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p25: isNat#(n__plus(V1,V2)) -> activate#(V1)
p26: isNat#(n__plus(V1,V2)) -> activate#(V2)
p27: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p28: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1))
p29: U22#(tt(),V1) -> isNat#(activate(V1))
p30: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p31: isNat#(n__s(V1)) -> activate#(V1)
p32: U22#(tt(),V1) -> activate#(V1)
p33: U21#(tt(),V1) -> activate#(V1)
p34: plus#(N,s(M)) -> U61#(isNat(M),M,N)
p35: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N))
p36: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N))
p37: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N))
p38: U64#(tt(),M,N) -> plus#(activate(N),activate(M))
p39: plus#(N,s(M)) -> isNat#(M)
p40: U64#(tt(),M,N) -> activate#(N)
p41: U64#(tt(),M,N) -> activate#(M)
p42: U63#(tt(),M,N) -> isNatKind#(activate(N))
p43: U63#(tt(),M,N) -> activate#(N)
p44: U63#(tt(),M,N) -> activate#(M)
p45: U62#(tt(),M,N) -> isNat#(activate(N))
p46: U62#(tt(),M,N) -> activate#(N)
p47: U62#(tt(),M,N) -> activate#(M)
p48: U61#(tt(),M,N) -> isNatKind#(activate(M))
p49: U61#(tt(),M,N) -> activate#(M)
p50: U61#(tt(),M,N) -> activate#(N)
p51: U31#(tt(),V2) -> activate#(V2)
p52: U12#(tt(),V1,V2) -> activate#(V2)

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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, r28, r29, r30, r31, r32, r33

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          U11#_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (147,46)
          tt_A() = (29,69)
          U12#_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x3 + (147,42)
          isNatKind_A(x1) = ((0,0),(1,0)) x1 + (32,34)
          activate_A(x1) = x1 + (0,70)
          isNatKind#_A(x1) = ((1,0),(0,0)) x1 + (146,287)
          n__plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,0)) x2
          U31#_A(x1,x2) = ((1,0),(0,0)) x2 + (146,287)
          activate#_A(x1) = ((1,0),(0,0)) x1 + (68,286)
          plus#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (67,144)
          |0|_A() = (82,0)
          U51#_A(x1,x2) = ((1,0),(0,0)) x2 + (147,144)
          isNat_A(x1) = (42,83)
          U52#_A(x1,x2) = ((1,0),(0,0)) x2 + (69,143)
          n__s_A(x1) = ((1,0),(1,0)) x1 + (147,142)
          isNat#_A(x1) = x1 + (148,144)
          U21#_A(x1,x2) = x2 + (149,286)
          U22#_A(x1,x2) = x2 + (149,215)
          s_A(x1) = ((1,0),(1,0)) x1 + (147,143)
          U61#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,1)) x3 + (148,358)
          U62#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,1)) x3 + (148,287)
          U63#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (146,287)
          U64#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (146,287)
          U16_A(x1) = ((0,0),(1,0)) x1 + (30,41)
          U15_A(x1,x2) = ((0,0),(1,0)) x1 + (31,55)
          U64_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (147,144)
          plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,0)) x2
          U14_A(x1,x2,x3) = ((1,0),(0,0)) x1 + (3,98)
          U63_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (147,145)
          U13_A(x1,x2,x3) = ((1,0),(1,1)) x1 + (7,1)
          U23_A(x1) = (29,69)
          U52_A(x1,x2) = x2 + (1,1)
          U62_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (147,145)
          U12_A(x1,x2,x3) = ((0,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (40,68)
          U22_A(x1,x2) = ((1,0),(1,1)) x1 + (1,4)
          U32_A(x1) = (30,29)
          U51_A(x1,x2) = ((1,0),(1,1)) x2 + (1,72)
          U61_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,1)) x3 + (147,146)
          U11_A(x1,x2,x3) = ((0,0),(1,0)) x1 + (41,40)
          U21_A(x1,x2) = (34,71)
          U31_A(x1,x2) = ((0,0),(1,0)) x1 + (31,1)
          U41_A(x1) = (30,70)
          n__0_A() = (82,0)
  
    precedence:
    
      U11# = tt = U12# = isNatKind = activate = isNatKind# = n__plus = U31# = activate# = plus# = |0| = U51# = isNat = U52# = n__s = isNat# = U21# = U22# = s = U61# = U62# = U63# = U64# = U16 = U15 = U64 = plus = U14 = U63 = U13 = U23 = U52 = U62 = U12 = U22 = U32 = U51 = U61 = U11 = U21 = U31 = U41 = n__0
    
    partial status:
  
      pi(U11#) = []
      pi(tt) = []
      pi(U12#) = []
      pi(isNatKind) = []
      pi(activate) = []
      pi(isNatKind#) = []
      pi(n__plus) = []
      pi(U31#) = []
      pi(activate#) = []
      pi(plus#) = []
      pi(|0|) = []
      pi(U51#) = []
      pi(isNat) = []
      pi(U52#) = []
      pi(n__s) = []
      pi(isNat#) = []
      pi(U21#) = []
      pi(U22#) = []
      pi(s) = []
      pi(U61#) = []
      pi(U62#) = []
      pi(U63#) = []
      pi(U64#) = []
      pi(U16) = []
      pi(U15) = []
      pi(U64) = []
      pi(plus) = []
      pi(U14) = []
      pi(U63) = []
      pi(U13) = []
      pi(U23) = []
      pi(U52) = []
      pi(U62) = []
      pi(U12) = []
      pi(U22) = []
      pi(U32) = []
      pi(U51) = []
      pi(U61) = []
      pi(U11) = []
      pi(U21) = []
      pi(U31) = []
      pi(U41) = []
      pi(n__0) = []

The next rules are strictly ordered:

  p17

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#(isNatKind(activate(V1)),activate(V1),activate(V2))
p2: U12#(tt(),V1,V2) -> isNatKind#(activate(V2))
p3: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2))
p4: U31#(tt(),V2) -> isNatKind#(activate(V2))
p5: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p6: isNatKind#(n__plus(V1,V2)) -> activate#(V1)
p7: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2))
p8: plus#(N,|0|()) -> U51#(isNat(N),N)
p9: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N))
p10: U52#(tt(),N) -> activate#(N)
p11: activate#(n__plus(X1,X2)) -> activate#(X1)
p12: activate#(n__plus(X1,X2)) -> activate#(X2)
p13: activate#(n__s(X)) -> activate#(X)
p14: U51#(tt(),N) -> isNatKind#(activate(N))
p15: isNatKind#(n__plus(V1,V2)) -> activate#(V2)
p16: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
p17: U51#(tt(),N) -> activate#(N)
p18: plus#(N,|0|()) -> isNat#(N)
p19: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2))
p20: U11#(tt(),V1,V2) -> isNatKind#(activate(V1))
p21: U11#(tt(),V1,V2) -> activate#(V1)
p22: U11#(tt(),V1,V2) -> activate#(V2)
p23: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p24: isNat#(n__plus(V1,V2)) -> activate#(V1)
p25: isNat#(n__plus(V1,V2)) -> activate#(V2)
p26: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p27: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1))
p28: U22#(tt(),V1) -> isNat#(activate(V1))
p29: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p30: isNat#(n__s(V1)) -> activate#(V1)
p31: U22#(tt(),V1) -> activate#(V1)
p32: U21#(tt(),V1) -> activate#(V1)
p33: plus#(N,s(M)) -> U61#(isNat(M),M,N)
p34: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N))
p35: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N))
p36: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N))
p37: U64#(tt(),M,N) -> plus#(activate(N),activate(M))
p38: plus#(N,s(M)) -> isNat#(M)
p39: U64#(tt(),M,N) -> activate#(N)
p40: U64#(tt(),M,N) -> activate#(M)
p41: U63#(tt(),M,N) -> isNatKind#(activate(N))
p42: U63#(tt(),M,N) -> activate#(N)
p43: U63#(tt(),M,N) -> activate#(M)
p44: U62#(tt(),M,N) -> isNat#(activate(N))
p45: U62#(tt(),M,N) -> activate#(N)
p46: U62#(tt(),M,N) -> activate#(M)
p47: U61#(tt(),M,N) -> isNatKind#(activate(M))
p48: U61#(tt(),M,N) -> activate#(M)
p49: U61#(tt(),M,N) -> activate#(N)
p50: U31#(tt(),V2) -> activate#(V2)
p51: U12#(tt(),V1,V2) -> activate#(V2)

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: activate(X) -> X

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, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32, p33, p34, p35, p36, p37, p38, p39, p40, p41, p42, p43, p44, p45, p46, p47, p48, p49, p50, p51}


-- Reduction pair.

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

p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2))
p2: U12#(tt(),V1,V2) -> activate#(V2)
p3: activate#(n__s(X)) -> activate#(X)
p4: activate#(n__plus(X1,X2)) -> activate#(X2)
p5: activate#(n__plus(X1,X2)) -> activate#(X1)
p6: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2))
p7: plus#(N,s(M)) -> isNat#(M)
p8: isNat#(n__s(V1)) -> activate#(V1)
p9: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p10: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
p11: isNatKind#(n__plus(V1,V2)) -> activate#(V2)
p12: isNatKind#(n__plus(V1,V2)) -> activate#(V1)
p13: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p14: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2))
p15: U31#(tt(),V2) -> activate#(V2)
p16: U31#(tt(),V2) -> isNatKind#(activate(V2))
p17: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p18: U21#(tt(),V1) -> activate#(V1)
p19: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1))
p20: U22#(tt(),V1) -> activate#(V1)
p21: U22#(tt(),V1) -> isNat#(activate(V1))
p22: isNat#(n__plus(V1,V2)) -> activate#(V2)
p23: isNat#(n__plus(V1,V2)) -> activate#(V1)
p24: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p25: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2))
p26: U11#(tt(),V1,V2) -> activate#(V2)
p27: U11#(tt(),V1,V2) -> activate#(V1)
p28: U11#(tt(),V1,V2) -> isNatKind#(activate(V1))
p29: plus#(N,s(M)) -> U61#(isNat(M),M,N)
p30: U61#(tt(),M,N) -> activate#(N)
p31: U61#(tt(),M,N) -> activate#(M)
p32: U61#(tt(),M,N) -> isNatKind#(activate(M))
p33: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N))
p34: U62#(tt(),M,N) -> activate#(M)
p35: U62#(tt(),M,N) -> activate#(N)
p36: U62#(tt(),M,N) -> isNat#(activate(N))
p37: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N))
p38: U63#(tt(),M,N) -> activate#(M)
p39: U63#(tt(),M,N) -> activate#(N)
p40: U63#(tt(),M,N) -> isNatKind#(activate(N))
p41: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N))
p42: U64#(tt(),M,N) -> activate#(M)
p43: U64#(tt(),M,N) -> activate#(N)
p44: U64#(tt(),M,N) -> plus#(activate(N),activate(M))
p45: plus#(N,|0|()) -> isNat#(N)
p46: plus#(N,|0|()) -> U51#(isNat(N),N)
p47: U51#(tt(),N) -> activate#(N)
p48: U51#(tt(),N) -> isNatKind#(activate(N))
p49: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N))
p50: U52#(tt(),N) -> activate#(N)
p51: U12#(tt(),V1,V2) -> isNatKind#(activate(V2))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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, r28, r29, r30, r31, r32, r33

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          U11#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (147,381)
          tt_A() = (221,654)
          U12#_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (145,0)
          isNatKind_A(x1) = ((1,0),(1,1)) x1 + (219,337)
          activate_A(x1) = x1 + (0,43)
          activate#_A(x1) = ((1,0),(0,0)) x1 + (73,180)
          n__s_A(x1) = ((1,0),(0,0)) x1 + (142,179)
          n__plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (74,39)
          plus#_A(x1,x2) = x1 + x2 + (81,92)
          s_A(x1) = ((1,0),(0,0)) x1 + (142,217)
          isNat#_A(x1) = x1 + (75,3)
          isNatKind#_A(x1) = ((1,0),(1,1)) x1 + (143,266)
          U31#_A(x1,x2) = ((1,0),(1,1)) x2 + (144,335)
          U21#_A(x1,x2) = ((1,0),(0,0)) x2 + (216,181)
          U22#_A(x1,x2) = ((1,0),(1,1)) x2 + (76,0)
          U61#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (222,309)
          isNat_A(x1) = ((1,0),(0,0)) x1 + (215,310)
          U62#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,1)) x3 + (221,265)
          U63#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (220,179)
          U64#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (219,0)
          |0|_A() = (227,88)
          U51#_A(x1,x2) = ((1,0),(1,0)) x2 + (228,180)
          U52#_A(x1,x2) = ((1,0),(0,0)) x2 + (74,180)
          U16_A(x1) = ((0,0),(1,0)) x1 + (222,440)
          U15_A(x1,x2) = (223,1)
          U64_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (216,219)
          plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (74,81)
          U14_A(x1,x2,x3) = (224,2)
          U63_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (216,221)
          U13_A(x1,x2,x3) = (225,44)
          U23_A(x1) = (222,1)
          U52_A(x1,x2) = ((1,0),(1,1)) x2 + (223,612)
          U62_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (216,2)
          U12_A(x1,x2,x3) = (226,45)
          U22_A(x1,x2) = (223,2)
          U32_A(x1) = ((1,0),(0,0)) x1 + (3,41)
          U51_A(x1,x2) = ((1,0),(0,0)) x2 + (225,42)
          U61_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (216,222)
          U11_A(x1,x2,x3) = x3 + (227,46)
          U21_A(x1,x2) = ((1,0),(0,0)) x1 + (3,3)
          U31_A(x1,x2) = ((1,0),(0,0)) x2 + (223,42)
          U41_A(x1) = (222,656)
          n__0_A() = (227,88)
  
    precedence:
    
      U12# = activate = n__s = U64# = U22 = U31 > isNat = U15 = U14 > isNat# = U61# = U62# > U12 = U11 > isNatKind > U21# > plus# = U51# > U52# > isNatKind# > U41 > U23 > tt = U32 > activate# = U31# = U63# > plus > U51 > U61 > U63 = U62 > U22# > |0| = U64 > s = U13 = U52 > U11# > n__plus = U16 = U21 = n__0
    
    partial status:
  
      pi(U11#) = []
      pi(tt) = []
      pi(U12#) = []
      pi(isNatKind) = [1]
      pi(activate) = []
      pi(activate#) = []
      pi(n__s) = []
      pi(n__plus) = []
      pi(plus#) = [2]
      pi(s) = []
      pi(isNat#) = []
      pi(isNatKind#) = [1]
      pi(U31#) = []
      pi(U21#) = []
      pi(U22#) = []
      pi(U61#) = []
      pi(isNat) = []
      pi(U62#) = []
      pi(U63#) = []
      pi(U64#) = []
      pi(|0|) = []
      pi(U51#) = []
      pi(U52#) = []
      pi(U16) = []
      pi(U15) = []
      pi(U64) = []
      pi(plus) = []
      pi(U14) = []
      pi(U63) = []
      pi(U13) = []
      pi(U23) = []
      pi(U52) = [2]
      pi(U62) = []
      pi(U12) = []
      pi(U22) = []
      pi(U32) = []
      pi(U51) = []
      pi(U61) = []
      pi(U11) = []
      pi(U21) = []
      pi(U31) = []
      pi(U41) = []
      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: U12#(tt(),V1,V2) -> activate#(V2)
p2: activate#(n__s(X)) -> activate#(X)
p3: activate#(n__plus(X1,X2)) -> activate#(X2)
p4: activate#(n__plus(X1,X2)) -> activate#(X1)
p5: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2))
p6: plus#(N,s(M)) -> isNat#(M)
p7: isNat#(n__s(V1)) -> activate#(V1)
p8: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p9: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
p10: isNatKind#(n__plus(V1,V2)) -> activate#(V2)
p11: isNatKind#(n__plus(V1,V2)) -> activate#(V1)
p12: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p13: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2))
p14: U31#(tt(),V2) -> activate#(V2)
p15: U31#(tt(),V2) -> isNatKind#(activate(V2))
p16: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p17: U21#(tt(),V1) -> activate#(V1)
p18: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1))
p19: U22#(tt(),V1) -> activate#(V1)
p20: U22#(tt(),V1) -> isNat#(activate(V1))
p21: isNat#(n__plus(V1,V2)) -> activate#(V2)
p22: isNat#(n__plus(V1,V2)) -> activate#(V1)
p23: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p24: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2))
p25: U11#(tt(),V1,V2) -> activate#(V2)
p26: U11#(tt(),V1,V2) -> activate#(V1)
p27: U11#(tt(),V1,V2) -> isNatKind#(activate(V1))
p28: plus#(N,s(M)) -> U61#(isNat(M),M,N)
p29: U61#(tt(),M,N) -> activate#(N)
p30: U61#(tt(),M,N) -> activate#(M)
p31: U61#(tt(),M,N) -> isNatKind#(activate(M))
p32: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N))
p33: U62#(tt(),M,N) -> activate#(M)
p34: U62#(tt(),M,N) -> activate#(N)
p35: U62#(tt(),M,N) -> isNat#(activate(N))
p36: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N))
p37: U63#(tt(),M,N) -> activate#(M)
p38: U63#(tt(),M,N) -> activate#(N)
p39: U63#(tt(),M,N) -> isNatKind#(activate(N))
p40: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N))
p41: U64#(tt(),M,N) -> activate#(M)
p42: U64#(tt(),M,N) -> activate#(N)
p43: U64#(tt(),M,N) -> plus#(activate(N),activate(M))
p44: plus#(N,|0|()) -> isNat#(N)
p45: plus#(N,|0|()) -> U51#(isNat(N),N)
p46: U51#(tt(),N) -> activate#(N)
p47: U51#(tt(),N) -> isNatKind#(activate(N))
p48: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N))
p49: U52#(tt(),N) -> activate#(N)
p50: U12#(tt(),V1,V2) -> isNatKind#(activate(V2))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, 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, p39, p40, p41, p42, p43, p44, p45, p46, p47, p48, p49}


-- Reduction pair.

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

p1: activate#(n__s(X)) -> activate#(X)
p2: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2))
p3: plus#(N,|0|()) -> U51#(isNat(N),N)
p4: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N))
p5: U52#(tt(),N) -> activate#(N)
p6: activate#(n__plus(X1,X2)) -> activate#(X1)
p7: activate#(n__plus(X1,X2)) -> activate#(X2)
p8: U51#(tt(),N) -> isNatKind#(activate(N))
p9: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2))
p10: U31#(tt(),V2) -> isNatKind#(activate(V2))
p11: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p12: isNatKind#(n__plus(V1,V2)) -> activate#(V1)
p13: isNatKind#(n__plus(V1,V2)) -> activate#(V2)
p14: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
p15: U31#(tt(),V2) -> activate#(V2)
p16: U51#(tt(),N) -> activate#(N)
p17: plus#(N,|0|()) -> isNat#(N)
p18: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2))
p19: U11#(tt(),V1,V2) -> isNatKind#(activate(V1))
p20: U11#(tt(),V1,V2) -> activate#(V1)
p21: U11#(tt(),V1,V2) -> activate#(V2)
p22: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p23: isNat#(n__plus(V1,V2)) -> activate#(V1)
p24: isNat#(n__plus(V1,V2)) -> activate#(V2)
p25: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p26: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1))
p27: U22#(tt(),V1) -> isNat#(activate(V1))
p28: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p29: isNat#(n__s(V1)) -> activate#(V1)
p30: U22#(tt(),V1) -> activate#(V1)
p31: U21#(tt(),V1) -> activate#(V1)
p32: plus#(N,s(M)) -> U61#(isNat(M),M,N)
p33: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N))
p34: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N))
p35: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N))
p36: U64#(tt(),M,N) -> plus#(activate(N),activate(M))
p37: plus#(N,s(M)) -> isNat#(M)
p38: U64#(tt(),M,N) -> activate#(N)
p39: U64#(tt(),M,N) -> activate#(M)
p40: U63#(tt(),M,N) -> isNatKind#(activate(N))
p41: U63#(tt(),M,N) -> activate#(N)
p42: U63#(tt(),M,N) -> activate#(M)
p43: U62#(tt(),M,N) -> isNat#(activate(N))
p44: U62#(tt(),M,N) -> activate#(N)
p45: U62#(tt(),M,N) -> activate#(M)
p46: U61#(tt(),M,N) -> isNatKind#(activate(M))
p47: U61#(tt(),M,N) -> activate#(M)
p48: U61#(tt(),M,N) -> activate#(N)

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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, r28, r29, r30, r31, r32, r33

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          activate#_A(x1) = x1 + (29,68)
          n__s_A(x1) = ((1,0),(1,0)) x1 + (30,75)
          n__plus_A(x1,x2) = ((1,0),(1,0)) x1 + x2 + (28,69)
          plus#_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (27,64)
          activate_A(x1) = x1 + (0,4)
          |0|_A() = (71,1)
          U51#_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (33,1)
          isNat_A(x1) = ((1,0),(1,0)) x1 + (63,0)
          tt_A() = (60,70)
          U52#_A(x1,x2) = ((1,0),(0,0)) x2 + (30,69)
          isNatKind_A(x1) = ((1,0),(0,0)) x1 + (59,5)
          isNatKind#_A(x1) = ((1,0),(0,0)) x1 + (32,1)
          U31#_A(x1,x2) = ((1,0),(0,0)) x2 + (32,1)
          isNat#_A(x1) = ((1,0),(0,0)) x1 + (4,66)
          U11#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (32,1)
          U21#_A(x1,x2) = x2 + (31,70)
          U22#_A(x1,x2) = ((1,0),(0,0)) x2 + (30,69)
          s_A(x1) = ((1,0),(1,0)) x1 + (30,76)
          U61#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + x3 + (56,67)
          U62#_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (55,7)
          U63#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (54,3)
          U64#_A(x1,x2,x3) = x2 + x3 + (53,69)
          U16_A(x1) = (61,71)
          U15_A(x1,x2) = (62,72)
          U64_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (58,105)
          plus_A(x1,x2) = ((1,0),(1,0)) x1 + x2 + (28,69)
          U14_A(x1,x2,x3) = x2 + (62,73)
          U63_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (58,106)
          U13_A(x1,x2,x3) = x1 + x2 + (2,8)
          U23_A(x1) = (61,71)
          U52_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (61,8)
          U62_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (58,107)
          U12_A(x1,x2,x3) = x2 + ((1,0),(0,0)) x3 + (61,18)
          U22_A(x1,x2) = (62,1)
          U32_A(x1) = ((1,0),(1,0)) x1 + (2,12)
          U51_A(x1,x2) = x2 + (62,0)
          U61_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (58,108)
          U11_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,0)) x3 + (61,23)
          U21_A(x1,x2) = (62,2)
          U31_A(x1,x2) = ((1,0),(1,0)) x1 + x2 + (2,7)
          U41_A(x1) = (61,4)
          n__0_A() = (71,1)
  
    precedence:
    
      U63 > U64 = U12 > U14 = U13 = U11 > isNat = U15 = U62 > U61 > U52 > n__s = activate = s = U64# > U23 = U22 = U21 > n__plus = |0| = plus > U51# > plus# > activate# = U52# = isNatKind# = U31# = isNat# = U11# = U21# = U22# = U61# = U62# = U63# > U51 > isNatKind = U41 > U32 = U31 > tt = U16 > n__0
    
    partial status:
  
      pi(activate#) = []
      pi(n__s) = []
      pi(n__plus) = [2]
      pi(plus#) = [2]
      pi(activate) = []
      pi(|0|) = []
      pi(U51#) = []
      pi(isNat) = []
      pi(tt) = []
      pi(U52#) = []
      pi(isNatKind) = []
      pi(isNatKind#) = []
      pi(U31#) = []
      pi(isNat#) = []
      pi(U11#) = []
      pi(U21#) = []
      pi(U22#) = []
      pi(s) = []
      pi(U61#) = []
      pi(U62#) = []
      pi(U63#) = []
      pi(U64#) = [3]
      pi(U16) = []
      pi(U15) = []
      pi(U64) = []
      pi(plus) = [2]
      pi(U14) = []
      pi(U63) = []
      pi(U13) = []
      pi(U23) = []
      pi(U52) = [2]
      pi(U62) = []
      pi(U12) = []
      pi(U22) = []
      pi(U32) = []
      pi(U51) = []
      pi(U61) = []
      pi(U11) = []
      pi(U21) = []
      pi(U31) = []
      pi(U41) = []
      pi(n__0) = []

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: activate#(n__s(X)) -> activate#(X)
p2: plus#(N,|0|()) -> U51#(isNat(N),N)
p3: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N))
p4: U52#(tt(),N) -> activate#(N)
p5: activate#(n__plus(X1,X2)) -> activate#(X1)
p6: activate#(n__plus(X1,X2)) -> activate#(X2)
p7: U51#(tt(),N) -> isNatKind#(activate(N))
p8: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2))
p9: U31#(tt(),V2) -> isNatKind#(activate(V2))
p10: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p11: isNatKind#(n__plus(V1,V2)) -> activate#(V1)
p12: isNatKind#(n__plus(V1,V2)) -> activate#(V2)
p13: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
p14: U31#(tt(),V2) -> activate#(V2)
p15: U51#(tt(),N) -> activate#(N)
p16: plus#(N,|0|()) -> isNat#(N)
p17: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2))
p18: U11#(tt(),V1,V2) -> isNatKind#(activate(V1))
p19: U11#(tt(),V1,V2) -> activate#(V1)
p20: U11#(tt(),V1,V2) -> activate#(V2)
p21: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1))
p22: isNat#(n__plus(V1,V2)) -> activate#(V1)
p23: isNat#(n__plus(V1,V2)) -> activate#(V2)
p24: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))
p25: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1))
p26: U22#(tt(),V1) -> isNat#(activate(V1))
p27: isNat#(n__s(V1)) -> isNatKind#(activate(V1))
p28: isNat#(n__s(V1)) -> activate#(V1)
p29: U22#(tt(),V1) -> activate#(V1)
p30: U21#(tt(),V1) -> activate#(V1)
p31: plus#(N,s(M)) -> U61#(isNat(M),M,N)
p32: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N))
p33: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N))
p34: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N))
p35: U64#(tt(),M,N) -> plus#(activate(N),activate(M))
p36: plus#(N,s(M)) -> isNat#(M)
p37: U64#(tt(),M,N) -> activate#(N)
p38: U64#(tt(),M,N) -> activate#(M)
p39: U63#(tt(),M,N) -> isNatKind#(activate(N))
p40: U63#(tt(),M,N) -> activate#(N)
p41: U63#(tt(),M,N) -> activate#(M)
p42: U62#(tt(),M,N) -> isNat#(activate(N))
p43: U62#(tt(),M,N) -> activate#(N)
p44: U62#(tt(),M,N) -> activate#(M)
p45: U61#(tt(),M,N) -> isNatKind#(activate(M))
p46: U61#(tt(),M,N) -> activate#(M)
p47: U61#(tt(),M,N) -> activate#(N)

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p31, p32, p33, p34, p35}
  {p24, p25, p26}
  {p8, p9, p10, p13}
  {p1, p5, p6}


-- Reduction pair.

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

p1: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N))
p2: U64#(tt(),M,N) -> plus#(activate(N),activate(M))
p3: plus#(N,s(M)) -> U61#(isNat(M),M,N)
p4: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N))
p5: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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, r28, r29, r30, r31, r32, r33

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          U63#_A(x1,x2,x3) = ((0,0),(1,0)) x2 + (1,4)
          tt_A() = (4,1)
          U64#_A(x1,x2,x3) = ((0,0),(1,0)) x2 + (1,3)
          isNatKind_A(x1) = ((0,0),(1,0)) x1 + (8,14)
          activate_A(x1) = ((1,0),(1,1)) x1 + (0,24)
          plus#_A(x1,x2) = ((0,0),(1,0)) x2 + (1,2)
          s_A(x1) = ((1,0),(0,0)) x1 + (9,11)
          U61#_A(x1,x2,x3) = ((0,0),(1,0)) x2 + (1,10)
          isNat_A(x1) = ((1,0),(0,0)) x1 + (2,16)
          U62#_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (1,1)
          U16_A(x1) = ((1,0),(1,1)) x1 + (3,1)
          U15_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (6,21)
          U64_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (35,12)
          plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (26,27)
          U14_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x3 + (3,48)
          U63_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (35,13)
          U13_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (12,49)
          U23_A(x1) = (5,2)
          U52_A(x1,x2) = x2 + (5,25)
          U62_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (35,23)
          U12_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (13,50)
          U22_A(x1,x2) = ((0,0),(1,0)) x1 + (6,13)
          U32_A(x1) = ((0,0),(1,0)) x1 + (5,1)
          U51_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (9,48)
          U61_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(1,1)) x3 + (35,44)
          U11_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (14,51)
          U21_A(x1,x2) = (7,15)
          U31_A(x1,x2) = ((0,0),(1,0)) x1 + (6,6)
          U41_A(x1) = ((1,0),(1,1)) x1
          |0|_A() = (5,17)
          n__0_A() = (5,17)
          n__plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (26,26)
          n__s_A(x1) = ((1,0),(0,0)) x1 + (9,10)
  
    precedence:
    
      isNatKind > U13 = U12 > U61 > tt = U64# = plus# = U61# = U14 = U23 > U63# = U62# > U62 > activate = plus = U52 = U51 = U31 = n__plus > U16 = U15 > U64 = U63 > s > U32 > isNat = U22 = U11 = U21 = U41 = |0| = n__0 = n__s
    
    partial status:
  
      pi(U63#) = []
      pi(tt) = []
      pi(U64#) = []
      pi(isNatKind) = []
      pi(activate) = [1]
      pi(plus#) = []
      pi(s) = []
      pi(U61#) = []
      pi(isNat) = []
      pi(U62#) = []
      pi(U16) = []
      pi(U15) = []
      pi(U64) = []
      pi(plus) = [2]
      pi(U14) = []
      pi(U63) = []
      pi(U13) = []
      pi(U23) = []
      pi(U52) = [2]
      pi(U62) = []
      pi(U12) = []
      pi(U22) = []
      pi(U32) = []
      pi(U51) = []
      pi(U61) = [3]
      pi(U11) = []
      pi(U21) = []
      pi(U31) = []
      pi(U41) = []
      pi(|0|) = []
      pi(n__0) = []
      pi(n__plus) = [2]
      pi(n__s) = []

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: U64#(tt(),M,N) -> plus#(activate(N),activate(M))
p2: plus#(N,s(M)) -> U61#(isNat(M),M,N)
p3: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N))
p4: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1))
p2: U22#(tt(),V1) -> isNat#(activate(V1))
p3: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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, r28, r29, r30, r31, r32, r33

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          U21#_A(x1,x2) = ((1,0),(1,1)) x2 + (9,23)
          tt_A() = (5,7)
          U22#_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (1,1)
          isNatKind_A(x1) = ((0,0),(1,0)) x1 + (8,0)
          activate_A(x1) = ((1,0),(1,1)) x1 + (0,22)
          isNat#_A(x1) = ((1,0),(1,1)) x1 + (1,35)
          n__s_A(x1) = ((1,0),(0,0)) x1 + (10,1)
          U16_A(x1) = ((1,0),(0,0)) x1 + (1,0)
          U15_A(x1,x2) = ((1,0),(0,0)) x2 + (3,8)
          isNat_A(x1) = ((1,0),(0,0)) x1 + (1,21)
          U14_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (4,9)
          U13_A(x1,x2,x3) = ((1,0),(1,1)) x1 + ((0,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (1,1)
          U23_A(x1) = (6,8)
          U64_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (28,13)
          s_A(x1) = ((1,0),(0,0)) x1 + (10,8)
          plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (18,2)
          U12_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (5,10)
          U22_A(x1,x2) = ((0,0),(1,0)) x1 + (7,4)
          U63_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (28,14)
          U11_A(x1,x2,x3) = x1 + ((0,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (9,4)
          U21_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (9,14)
          U52_A(x1,x2) = ((1,0),(0,0)) x2 + (1,18)
          U62_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (28,10)
          U32_A(x1) = (6,8)
          U51_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (2,14)
          U61_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (28,19)
          n__0_A() = (6,1)
          n__plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (18,1)
          U31_A(x1,x2) = (7,9)
          U41_A(x1) = ((0,0),(1,0)) x1 + (6,3)
          |0|_A() = (6,14)
  
    precedence:
    
      activate = U23 = U64 = U63 = U52 = U62 = U51 = U61 > isNatKind = isNat# = n__s = U16 = U15 = U14 = U13 = s = U12 = U11 = U32 = U31 = U41 > tt > plus > U21# = U22# = isNat = U22 = U21 = n__0 = |0| > n__plus
    
    partial status:
  
      pi(U21#) = [2]
      pi(tt) = []
      pi(U22#) = []
      pi(isNatKind) = []
      pi(activate) = []
      pi(isNat#) = [1]
      pi(n__s) = []
      pi(U16) = []
      pi(U15) = []
      pi(isNat) = []
      pi(U14) = []
      pi(U13) = [1]
      pi(U23) = []
      pi(U64) = []
      pi(s) = []
      pi(plus) = []
      pi(U12) = []
      pi(U22) = []
      pi(U63) = []
      pi(U11) = []
      pi(U21) = []
      pi(U52) = []
      pi(U62) = []
      pi(U32) = []
      pi(U51) = []
      pi(U61) = []
      pi(n__0) = []
      pi(n__plus) = []
      pi(U31) = []
      pi(U41) = []
      pi(|0|) = []

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2))
p2: U31#(tt(),V2) -> isNatKind#(activate(V2))
p3: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
p4: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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, r28, r29, r30, r31, r32, r33

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          isNatKind#_A(x1) = ((1,0),(0,0)) x1 + (1,19)
          n__plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (0,13)
          U31#_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (1,12)
          isNatKind_A(x1) = ((1,0),(0,0)) x1 + (0,6)
          activate_A(x1) = ((1,0),(1,1)) x1 + (0,12)
          tt_A() = (6,1)
          n__s_A(x1) = ((1,0),(0,0)) x1 + (7,8)
          U16_A(x1) = (7,2)
          U15_A(x1,x2) = (8,3)
          isNat_A(x1) = ((1,0),(1,0)) x1 + (0,33)
          U14_A(x1,x2,x3) = ((0,0),(1,0)) x3 + (9,4)
          U13_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x3 + (4,5)
          U23_A(x1) = (6,2)
          U64_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (7,10)
          s_A(x1) = ((1,0),(0,0)) x1 + (7,9)
          plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (0,25)
          U12_A(x1,x2,x3) = ((1,0),(1,0)) x3 + (5,13)
          U22_A(x1,x2) = (6,13)
          U63_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (7,11)
          U11_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x3 + (0,14)
          U21_A(x1,x2) = (6,14)
          U52_A(x1,x2) = ((1,0),(1,1)) x2 + (0,13)
          U62_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (7,34)
          U32_A(x1) = (6,2)
          U51_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (1,33)
          U61_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (7,31)
          n__0_A() = (7,16)
          U31_A(x1,x2) = ((1,0),(0,0)) x1 + (0,3)
          U41_A(x1) = (6,7)
          |0|_A() = (7,34)
  
    precedence:
    
      activate = U62 = U41 > isNat = U13 = U12 = U11 > U15 = U14 > isNatKind > tt = U16 = U23 = U32 = U31 > U22 = U21 > isNatKind# > U31# > U63 > U64 > |0| > n__plus = n__s = s = plus = U52 = U51 = U61 = n__0
    
    partial status:
  
      pi(isNatKind#) = []
      pi(n__plus) = []
      pi(U31#) = []
      pi(isNatKind) = []
      pi(activate) = []
      pi(tt) = []
      pi(n__s) = []
      pi(U16) = []
      pi(U15) = []
      pi(isNat) = []
      pi(U14) = []
      pi(U13) = []
      pi(U23) = []
      pi(U64) = []
      pi(s) = []
      pi(plus) = []
      pi(U12) = []
      pi(U22) = []
      pi(U63) = []
      pi(U11) = []
      pi(U21) = []
      pi(U52) = []
      pi(U62) = []
      pi(U32) = []
      pi(U51) = []
      pi(U61) = []
      pi(n__0) = []
      pi(U31) = []
      pi(U41) = []
      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: U31#(tt(),V2) -> isNatKind#(activate(V2))
p2: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))
p3: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1))

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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: 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(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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, r28, r29, r30, r31, r32, r33

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          isNatKind#_A(x1) = ((1,0),(0,0)) x1 + (1,1)
          n__s_A(x1) = ((1,0),(0,0)) x1 + (71,68)
          activate_A(x1) = x1 + (0,22)
          n__plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (9,30)
          U16_A(x1) = ((0,0),(1,0)) x1 + (70,1)
          tt_A() = (69,0)
          U15_A(x1,x2) = ((0,0),(1,0)) x2 + (71,4)
          isNat_A(x1) = ((1,0),(0,0)) x1 + (2,32)
          U14_A(x1,x2,x3) = ((1,0),(0,0)) x1 + x2 + (3,0)
          U13_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (7,0)
          isNatKind_A(x1) = ((1,0),(1,0)) x1 + (3,33)
          U23_A(x1) = (70,1)
          U32_A(x1) = ((1,0),(1,0)) x1 + (7,1)
          U64_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (80,1)
          s_A(x1) = ((1,0),(0,0)) x1 + (71,69)
          plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (9,30)
          U12_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (7,0)
          U22_A(x1,x2) = (138,33)
          U31_A(x1,x2) = ((1,0),(1,1)) x2 + (11,21)
          U41_A(x1) = (70,69)
          U63_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (80,5)
          U11_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (8,31)
          U21_A(x1,x2) = x1 + (69,34)
          U52_A(x1,x2) = ((1,0),(1,1)) x2 + (70,21)
          U62_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,1)) x3 + (80,6)
          n__0_A() = (67,1)
          U51_A(x1,x2) = ((1,0),(0,0)) x2 + (75,21)
          U61_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,1)) x3 + (80,29)
          |0|_A() = (67,2)
  
    precedence:
    
      U23 = U22 > U16 = tt = isNat = U32 = U31 = U41 = U11 > isNatKind > isNatKind# > activate = n__plus = plus = U52 > U61 > U13 = U12 = U62 > n__0 = |0| > n__s = U64 = s = U63 = U51 > U15 = U14 = U21
    
    partial status:
  
      pi(isNatKind#) = []
      pi(n__s) = []
      pi(activate) = []
      pi(n__plus) = []
      pi(U16) = []
      pi(tt) = []
      pi(U15) = []
      pi(isNat) = []
      pi(U14) = []
      pi(U13) = []
      pi(isNatKind) = []
      pi(U23) = []
      pi(U32) = []
      pi(U64) = []
      pi(s) = []
      pi(plus) = []
      pi(U12) = []
      pi(U22) = []
      pi(U31) = []
      pi(U41) = []
      pi(U63) = []
      pi(U11) = []
      pi(U21) = []
      pi(U52) = [2]
      pi(U62) = []
      pi(n__0) = []
      pi(U51) = []
      pi(U61) = []
      pi(|0|) = []

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(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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, r28, r29, r30, r31, r32, r33

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          isNatKind#_A(x1) = ((1,0),(1,0)) x1 + (14,3)
          n__s_A(x1) = ((1,0),(0,0)) x1 + (13,2)
          activate_A(x1) = x1 + (0,24)
          U16_A(x1) = ((0,0),(1,0)) x1 + (5,6)
          tt_A() = (4,6)
          U15_A(x1,x2) = ((0,0),(1,0)) x2 + (6,8)
          isNat_A(x1) = ((1,0),(0,0)) x1 + (1,9)
          U14_A(x1,x2,x3) = ((0,0),(1,0)) x3 + (7,25)
          U13_A(x1,x2,x3) = ((0,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (8,26)
          isNatKind_A(x1) = ((1,0),(1,0)) x1 + (1,12)
          U23_A(x1) = (5,7)
          U32_A(x1) = ((0,0),(1,0)) x1 + (5,1)
          U64_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (24,8)
          s_A(x1) = ((1,0),(0,0)) x1 + (13,7)
          plus_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (11,12)
          U12_A(x1,x2,x3) = (9,5)
          U22_A(x1,x2) = ((0,0),(1,0)) x2 + (6,2)
          U31_A(x1,x2) = ((0,0),(1,0)) x2 + (6,3)
          U41_A(x1) = (5,26)
          U63_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (24,9)
          U11_A(x1,x2,x3) = (10,8)
          U21_A(x1,x2) = (13,1)
          U52_A(x1,x2) = ((1,0),(0,0)) x2 + (1,7)
          U62_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (24,10)
          n__0_A() = (3,1)
          n__plus_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (11,0)
          U51_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (2,21)
          U61_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (24,11)
          |0|_A() = (3,1)
  
    precedence:
    
      U41 = U63 > U62 > U23 > isNatKind > U32 = U31 > U64 > tt > isNat = n__0 = |0| > activate > s > U15 = U14 = U13 = U12 = U11 = U61 > plus = n__plus > isNatKind# > n__s = U22 = U21 = U52 = U51 > U16
    
    partial status:
  
      pi(isNatKind#) = []
      pi(n__s) = []
      pi(activate) = [1]
      pi(U16) = []
      pi(tt) = []
      pi(U15) = []
      pi(isNat) = []
      pi(U14) = []
      pi(U13) = []
      pi(isNatKind) = []
      pi(U23) = []
      pi(U32) = []
      pi(U64) = []
      pi(s) = []
      pi(plus) = []
      pi(U12) = []
      pi(U22) = []
      pi(U31) = []
      pi(U41) = []
      pi(U63) = []
      pi(U11) = []
      pi(U21) = []
      pi(U52) = []
      pi(U62) = []
      pi(n__0) = []
      pi(n__plus) = []
      pi(U51) = []
      pi(U61) = []
      pi(|0|) = []

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: activate#(n__s(X)) -> activate#(X)
p2: activate#(n__plus(X1,X2)) -> activate#(X2)
p3: activate#(n__plus(X1,X2)) -> activate#(X1)

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: activate(X) -> X

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          activate#_A(x1) = ((1,0),(1,0)) x1 + (2,2)
          n__s_A(x1) = ((1,0),(0,0)) x1 + (3,1)
          n__plus_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (1,1)
  
    precedence:
    
      activate# = n__s = n__plus
    
    partial status:
  
      pi(activate#) = []
      pi(n__s) = []
      pi(n__plus) = []

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: activate#(n__plus(X1,X2)) -> activate#(X2)
p2: activate#(n__plus(X1,X2)) -> activate#(X1)

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

p1: activate#(n__plus(X1,X2)) -> activate#(X2)
p2: activate#(n__plus(X1,X2)) -> activate#(X1)

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: activate(X) -> X

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          activate#_A(x1) = ((1,0),(0,0)) x1
          n__plus_A(x1,x2) = x1 + ((1,0),(1,0)) x2 + (1,1)
  
    precedence:
    
      n__plus > activate#
    
    partial status:
  
      pi(activate#) = []
      pi(n__plus) = [1]

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: activate#(n__plus(X1,X2)) -> activate#(X1)

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: 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: activate#(n__plus(X1,X2)) -> activate#(X1)

and R consists of:

r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
r5: U15(tt(),V2) -> U16(isNat(activate(V2)))
r6: U16(tt()) -> tt()
r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
r8: U22(tt(),V1) -> U23(isNat(activate(V1)))
r9: U23(tt()) -> tt()
r10: U31(tt(),V2) -> U32(isNatKind(activate(V2)))
r11: U32(tt()) -> tt()
r12: U41(tt()) -> tt()
r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
r14: U52(tt(),N) -> activate(N)
r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
r19: isNat(n__0()) -> tt()
r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
r22: isNatKind(n__0()) -> tt()
r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
r25: plus(N,|0|()) -> U51(isNat(N),N)
r26: plus(N,s(M)) -> U61(isNat(M),M,N)
r27: |0|() -> n__0()
r28: plus(X1,X2) -> n__plus(X1,X2)
r29: s(X) -> n__s(X)
r30: activate(n__0()) -> |0|()
r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
r32: activate(n__s(X)) -> s(activate(X))
r33: activate(X) -> X

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          activate#_A(x1) = ((1,0),(1,1)) x1
          n__plus_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (1,1)
  
    precedence:
    
      activate# > n__plus
    
    partial status:
  
      pi(activate#) = [1]
      pi(n__plus) = [1, 2]

The next rules are strictly ordered:

  p1

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