Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

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)
0n__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

Q is empty.


QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

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)
0n__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

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

U111(tt, V1, V2) → ACTIVATE(V2)
U111(tt, V1, V2) → ISNATKIND(activate(V1))
ISNATKIND(n__s(V1)) → U411(isNatKind(activate(V1)))
U211(tt, V1) → ISNATKIND(activate(V1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
U621(tt, M, N) → ACTIVATE(M)
ACTIVATE(n__0) → 01
U151(tt, V2) → ACTIVATE(V2)
ISNATKIND(n__s(V1)) → ISNATKIND(activate(V1))
U121(tt, V1, V2) → ACTIVATE(V2)
PLUS(N, s(M)) → U611(isNat(M), M, N)
U641(tt, M, N) → ACTIVATE(N)
ACTIVATE(n__plus(X1, X2)) → ACTIVATE(X1)
U141(tt, V1, V2) → ACTIVATE(V1)
ACTIVATE(n__s(X)) → S(activate(X))
U611(tt, M, N) → ACTIVATE(M)
ISNAT(n__plus(V1, V2)) → U111(isNatKind(activate(V1)), activate(V1), activate(V2))
ISNAT(n__s(V1)) → ACTIVATE(V1)
U111(tt, V1, V2) → ACTIVATE(V1)
U311(tt, V2) → U321(isNatKind(activate(V2)))
U211(tt, V1) → U221(isNatKind(activate(V1)), activate(V1))
U121(tt, V1, V2) → U131(isNatKind(activate(V2)), activate(V1), activate(V2))
U611(tt, M, N) → ACTIVATE(N)
ISNAT(n__plus(V1, V2)) → ACTIVATE(V1)
U521(tt, N) → ACTIVATE(N)
U141(tt, V1, V2) → ISNAT(activate(V1))
U311(tt, V2) → ISNATKIND(activate(V2))
U151(tt, V2) → ISNAT(activate(V2))
ISNATKIND(n__plus(V1, V2)) → U311(isNatKind(activate(V1)), activate(V2))
U611(tt, M, N) → ISNATKIND(activate(M))
ISNAT(n__s(V1)) → U211(isNatKind(activate(V1)), activate(V1))
ACTIVATE(n__plus(X1, X2)) → ACTIVATE(X2)
U141(tt, V1, V2) → U151(isNat(activate(V1)), activate(V2))
U631(tt, M, N) → U641(isNatKind(activate(N)), activate(M), activate(N))
U221(tt, V1) → U231(isNat(activate(V1)))
U111(tt, V1, V2) → U121(isNatKind(activate(V1)), activate(V1), activate(V2))
U121(tt, V1, V2) → ISNATKIND(activate(V2))
U621(tt, M, N) → U631(isNat(activate(N)), activate(M), activate(N))
U611(tt, M, N) → U621(isNatKind(activate(M)), activate(M), activate(N))
ISNAT(n__s(V1)) → ISNATKIND(activate(V1))
U641(tt, M, N) → ACTIVATE(M)
U641(tt, M, N) → S(plus(activate(N), activate(M)))
U631(tt, M, N) → ACTIVATE(N)
PLUS(N, s(M)) → ISNAT(M)
ISNATKIND(n__plus(V1, V2)) → ACTIVATE(V1)
U511(tt, N) → ACTIVATE(N)
U131(tt, V1, V2) → U141(isNatKind(activate(V2)), activate(V1), activate(V2))
U311(tt, V2) → ACTIVATE(V2)
ISNATKIND(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__plus(X1, X2)) → PLUS(activate(X1), activate(X2))
ISNAT(n__plus(V1, V2)) → ISNATKIND(activate(V1))
U121(tt, V1, V2) → ACTIVATE(V1)
U511(tt, N) → ISNATKIND(activate(N))
U631(tt, M, N) → ISNATKIND(activate(N))
PLUS(N, 0) → ISNAT(N)
U141(tt, V1, V2) → ACTIVATE(V2)
ISNATKIND(n__plus(V1, V2)) → ISNATKIND(activate(V1))
U621(tt, M, N) → ISNAT(activate(N))
U221(tt, V1) → ISNAT(activate(V1))
ISNATKIND(n__plus(V1, V2)) → ACTIVATE(V2)
U221(tt, V1) → ACTIVATE(V1)
U131(tt, V1, V2) → ACTIVATE(V1)
ISNAT(n__plus(V1, V2)) → ACTIVATE(V2)
U621(tt, M, N) → ACTIVATE(N)
U151(tt, V2) → U161(isNat(activate(V2)))
U211(tt, V1) → ACTIVATE(V1)
U131(tt, V1, V2) → ISNATKIND(activate(V2))
U631(tt, M, N) → ACTIVATE(M)
U641(tt, M, N) → PLUS(activate(N), activate(M))
U511(tt, N) → U521(isNatKind(activate(N)), activate(N))
U131(tt, V1, V2) → ACTIVATE(V2)
PLUS(N, 0) → U511(isNat(N), N)

The TRS R consists of the following rules:

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)
0n__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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U111(tt, V1, V2) → ACTIVATE(V2)
U111(tt, V1, V2) → ISNATKIND(activate(V1))
ISNATKIND(n__s(V1)) → U411(isNatKind(activate(V1)))
U211(tt, V1) → ISNATKIND(activate(V1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
U621(tt, M, N) → ACTIVATE(M)
ACTIVATE(n__0) → 01
U151(tt, V2) → ACTIVATE(V2)
ISNATKIND(n__s(V1)) → ISNATKIND(activate(V1))
U121(tt, V1, V2) → ACTIVATE(V2)
PLUS(N, s(M)) → U611(isNat(M), M, N)
U641(tt, M, N) → ACTIVATE(N)
ACTIVATE(n__plus(X1, X2)) → ACTIVATE(X1)
U141(tt, V1, V2) → ACTIVATE(V1)
ACTIVATE(n__s(X)) → S(activate(X))
U611(tt, M, N) → ACTIVATE(M)
ISNAT(n__plus(V1, V2)) → U111(isNatKind(activate(V1)), activate(V1), activate(V2))
ISNAT(n__s(V1)) → ACTIVATE(V1)
U111(tt, V1, V2) → ACTIVATE(V1)
U311(tt, V2) → U321(isNatKind(activate(V2)))
U211(tt, V1) → U221(isNatKind(activate(V1)), activate(V1))
U121(tt, V1, V2) → U131(isNatKind(activate(V2)), activate(V1), activate(V2))
U611(tt, M, N) → ACTIVATE(N)
ISNAT(n__plus(V1, V2)) → ACTIVATE(V1)
U521(tt, N) → ACTIVATE(N)
U141(tt, V1, V2) → ISNAT(activate(V1))
U311(tt, V2) → ISNATKIND(activate(V2))
U151(tt, V2) → ISNAT(activate(V2))
ISNATKIND(n__plus(V1, V2)) → U311(isNatKind(activate(V1)), activate(V2))
U611(tt, M, N) → ISNATKIND(activate(M))
ISNAT(n__s(V1)) → U211(isNatKind(activate(V1)), activate(V1))
ACTIVATE(n__plus(X1, X2)) → ACTIVATE(X2)
U141(tt, V1, V2) → U151(isNat(activate(V1)), activate(V2))
U631(tt, M, N) → U641(isNatKind(activate(N)), activate(M), activate(N))
U221(tt, V1) → U231(isNat(activate(V1)))
U111(tt, V1, V2) → U121(isNatKind(activate(V1)), activate(V1), activate(V2))
U121(tt, V1, V2) → ISNATKIND(activate(V2))
U621(tt, M, N) → U631(isNat(activate(N)), activate(M), activate(N))
U611(tt, M, N) → U621(isNatKind(activate(M)), activate(M), activate(N))
ISNAT(n__s(V1)) → ISNATKIND(activate(V1))
U641(tt, M, N) → ACTIVATE(M)
U641(tt, M, N) → S(plus(activate(N), activate(M)))
U631(tt, M, N) → ACTIVATE(N)
PLUS(N, s(M)) → ISNAT(M)
ISNATKIND(n__plus(V1, V2)) → ACTIVATE(V1)
U511(tt, N) → ACTIVATE(N)
U131(tt, V1, V2) → U141(isNatKind(activate(V2)), activate(V1), activate(V2))
U311(tt, V2) → ACTIVATE(V2)
ISNATKIND(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__plus(X1, X2)) → PLUS(activate(X1), activate(X2))
ISNAT(n__plus(V1, V2)) → ISNATKIND(activate(V1))
U121(tt, V1, V2) → ACTIVATE(V1)
U511(tt, N) → ISNATKIND(activate(N))
U631(tt, M, N) → ISNATKIND(activate(N))
PLUS(N, 0) → ISNAT(N)
U141(tt, V1, V2) → ACTIVATE(V2)
ISNATKIND(n__plus(V1, V2)) → ISNATKIND(activate(V1))
U621(tt, M, N) → ISNAT(activate(N))
U221(tt, V1) → ISNAT(activate(V1))
ISNATKIND(n__plus(V1, V2)) → ACTIVATE(V2)
U221(tt, V1) → ACTIVATE(V1)
U131(tt, V1, V2) → ACTIVATE(V1)
ISNAT(n__plus(V1, V2)) → ACTIVATE(V2)
U621(tt, M, N) → ACTIVATE(N)
U151(tt, V2) → U161(isNat(activate(V2)))
U211(tt, V1) → ACTIVATE(V1)
U131(tt, V1, V2) → ISNATKIND(activate(V2))
U631(tt, M, N) → ACTIVATE(M)
U641(tt, M, N) → PLUS(activate(N), activate(M))
U511(tt, N) → U521(isNatKind(activate(N)), activate(N))
U131(tt, V1, V2) → ACTIVATE(V2)
PLUS(N, 0) → U511(isNat(N), N)

The TRS R consists of the following rules:

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)
0n__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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 7 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
QDP
          ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

U111(tt, V1, V2) → ACTIVATE(V2)
U111(tt, V1, V2) → ISNATKIND(activate(V1))
U211(tt, V1) → ISNATKIND(activate(V1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
U621(tt, M, N) → ACTIVATE(M)
U151(tt, V2) → ACTIVATE(V2)
U121(tt, V1, V2) → ACTIVATE(V2)
ISNATKIND(n__s(V1)) → ISNATKIND(activate(V1))
PLUS(N, s(M)) → U611(isNat(M), M, N)
U641(tt, M, N) → ACTIVATE(N)
ACTIVATE(n__plus(X1, X2)) → ACTIVATE(X1)
U141(tt, V1, V2) → ACTIVATE(V1)
U611(tt, M, N) → ACTIVATE(M)
ISNAT(n__plus(V1, V2)) → U111(isNatKind(activate(V1)), activate(V1), activate(V2))
ISNAT(n__s(V1)) → ACTIVATE(V1)
U111(tt, V1, V2) → ACTIVATE(V1)
U211(tt, V1) → U221(isNatKind(activate(V1)), activate(V1))
U611(tt, M, N) → ACTIVATE(N)
U121(tt, V1, V2) → U131(isNatKind(activate(V2)), activate(V1), activate(V2))
U521(tt, N) → ACTIVATE(N)
ISNAT(n__plus(V1, V2)) → ACTIVATE(V1)
U141(tt, V1, V2) → ISNAT(activate(V1))
U311(tt, V2) → ISNATKIND(activate(V2))
U151(tt, V2) → ISNAT(activate(V2))
ISNATKIND(n__plus(V1, V2)) → U311(isNatKind(activate(V1)), activate(V2))
U611(tt, M, N) → ISNATKIND(activate(M))
ISNAT(n__s(V1)) → U211(isNatKind(activate(V1)), activate(V1))
ACTIVATE(n__plus(X1, X2)) → ACTIVATE(X2)
U141(tt, V1, V2) → U151(isNat(activate(V1)), activate(V2))
U631(tt, M, N) → U641(isNatKind(activate(N)), activate(M), activate(N))
U111(tt, V1, V2) → U121(isNatKind(activate(V1)), activate(V1), activate(V2))
U121(tt, V1, V2) → ISNATKIND(activate(V2))
U621(tt, M, N) → U631(isNat(activate(N)), activate(M), activate(N))
U611(tt, M, N) → U621(isNatKind(activate(M)), activate(M), activate(N))
ISNAT(n__s(V1)) → ISNATKIND(activate(V1))
U641(tt, M, N) → ACTIVATE(M)
U631(tt, M, N) → ACTIVATE(N)
PLUS(N, s(M)) → ISNAT(M)
U511(tt, N) → ACTIVATE(N)
ISNATKIND(n__plus(V1, V2)) → ACTIVATE(V1)
U131(tt, V1, V2) → U141(isNatKind(activate(V2)), activate(V1), activate(V2))
U311(tt, V2) → ACTIVATE(V2)
ISNATKIND(n__s(V1)) → ACTIVATE(V1)
ISNAT(n__plus(V1, V2)) → ISNATKIND(activate(V1))
ACTIVATE(n__plus(X1, X2)) → PLUS(activate(X1), activate(X2))
U121(tt, V1, V2) → ACTIVATE(V1)
U511(tt, N) → ISNATKIND(activate(N))
U631(tt, M, N) → ISNATKIND(activate(N))
PLUS(N, 0) → ISNAT(N)
U141(tt, V1, V2) → ACTIVATE(V2)
ISNATKIND(n__plus(V1, V2)) → ISNATKIND(activate(V1))
U621(tt, M, N) → ISNAT(activate(N))
U221(tt, V1) → ISNAT(activate(V1))
U131(tt, V1, V2) → ACTIVATE(V1)
ISNATKIND(n__plus(V1, V2)) → ACTIVATE(V2)
U221(tt, V1) → ACTIVATE(V1)
ISNAT(n__plus(V1, V2)) → ACTIVATE(V2)
U621(tt, M, N) → ACTIVATE(N)
U211(tt, V1) → ACTIVATE(V1)
U131(tt, V1, V2) → ISNATKIND(activate(V2))
U641(tt, M, N) → PLUS(activate(N), activate(M))
U631(tt, M, N) → ACTIVATE(M)
U511(tt, N) → U521(isNatKind(activate(N)), activate(N))
U131(tt, V1, V2) → ACTIVATE(V2)
PLUS(N, 0) → U511(isNat(N), N)

The TRS R consists of the following rules:

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)
0n__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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


ACTIVATE(n__plus(X1, X2)) → ACTIVATE(X1)
ISNAT(n__plus(V1, V2)) → U111(isNatKind(activate(V1)), activate(V1), activate(V2))
ISNAT(n__plus(V1, V2)) → ACTIVATE(V1)
ISNATKIND(n__plus(V1, V2)) → U311(isNatKind(activate(V1)), activate(V2))
ACTIVATE(n__plus(X1, X2)) → ACTIVATE(X2)
ISNATKIND(n__plus(V1, V2)) → ACTIVATE(V1)
ISNAT(n__plus(V1, V2)) → ISNATKIND(activate(V1))
ACTIVATE(n__plus(X1, X2)) → PLUS(activate(X1), activate(X2))
ISNATKIND(n__plus(V1, V2)) → ISNATKIND(activate(V1))
ISNATKIND(n__plus(V1, V2)) → ACTIVATE(V2)
ISNAT(n__plus(V1, V2)) → ACTIVATE(V2)
The remaining pairs can at least be oriented weakly.

U111(tt, V1, V2) → ACTIVATE(V2)
U111(tt, V1, V2) → ISNATKIND(activate(V1))
U211(tt, V1) → ISNATKIND(activate(V1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
U621(tt, M, N) → ACTIVATE(M)
U151(tt, V2) → ACTIVATE(V2)
U121(tt, V1, V2) → ACTIVATE(V2)
ISNATKIND(n__s(V1)) → ISNATKIND(activate(V1))
PLUS(N, s(M)) → U611(isNat(M), M, N)
U641(tt, M, N) → ACTIVATE(N)
U141(tt, V1, V2) → ACTIVATE(V1)
U611(tt, M, N) → ACTIVATE(M)
ISNAT(n__s(V1)) → ACTIVATE(V1)
U111(tt, V1, V2) → ACTIVATE(V1)
U211(tt, V1) → U221(isNatKind(activate(V1)), activate(V1))
U611(tt, M, N) → ACTIVATE(N)
U121(tt, V1, V2) → U131(isNatKind(activate(V2)), activate(V1), activate(V2))
U521(tt, N) → ACTIVATE(N)
U141(tt, V1, V2) → ISNAT(activate(V1))
U311(tt, V2) → ISNATKIND(activate(V2))
U151(tt, V2) → ISNAT(activate(V2))
U611(tt, M, N) → ISNATKIND(activate(M))
ISNAT(n__s(V1)) → U211(isNatKind(activate(V1)), activate(V1))
U141(tt, V1, V2) → U151(isNat(activate(V1)), activate(V2))
U631(tt, M, N) → U641(isNatKind(activate(N)), activate(M), activate(N))
U111(tt, V1, V2) → U121(isNatKind(activate(V1)), activate(V1), activate(V2))
U121(tt, V1, V2) → ISNATKIND(activate(V2))
U621(tt, M, N) → U631(isNat(activate(N)), activate(M), activate(N))
U611(tt, M, N) → U621(isNatKind(activate(M)), activate(M), activate(N))
ISNAT(n__s(V1)) → ISNATKIND(activate(V1))
U641(tt, M, N) → ACTIVATE(M)
U631(tt, M, N) → ACTIVATE(N)
PLUS(N, s(M)) → ISNAT(M)
U511(tt, N) → ACTIVATE(N)
U131(tt, V1, V2) → U141(isNatKind(activate(V2)), activate(V1), activate(V2))
U311(tt, V2) → ACTIVATE(V2)
ISNATKIND(n__s(V1)) → ACTIVATE(V1)
U121(tt, V1, V2) → ACTIVATE(V1)
U511(tt, N) → ISNATKIND(activate(N))
U631(tt, M, N) → ISNATKIND(activate(N))
PLUS(N, 0) → ISNAT(N)
U141(tt, V1, V2) → ACTIVATE(V2)
U621(tt, M, N) → ISNAT(activate(N))
U221(tt, V1) → ISNAT(activate(V1))
U131(tt, V1, V2) → ACTIVATE(V1)
U221(tt, V1) → ACTIVATE(V1)
U621(tt, M, N) → ACTIVATE(N)
U211(tt, V1) → ACTIVATE(V1)
U131(tt, V1, V2) → ISNATKIND(activate(V2))
U641(tt, M, N) → PLUS(activate(N), activate(M))
U631(tt, M, N) → ACTIVATE(M)
U511(tt, N) → U521(isNatKind(activate(N)), activate(N))
U131(tt, V1, V2) → ACTIVATE(V2)
PLUS(N, 0) → U511(isNat(N), N)
Used ordering: Polynomial interpretation [25]:

POL(0) = 0   
POL(ACTIVATE(x1)) = x1   
POL(ISNAT(x1)) = x1   
POL(ISNATKIND(x1)) = x1   
POL(PLUS(x1, x2)) = x1 + x2   
POL(U11(x1, x2, x3)) = x2 + x3   
POL(U111(x1, x2, x3)) = x2 + x3   
POL(U12(x1, x2, x3)) = x2 + x3   
POL(U121(x1, x2, x3)) = x2 + x3   
POL(U13(x1, x2, x3)) = x2 + x3   
POL(U131(x1, x2, x3)) = x2 + x3   
POL(U14(x1, x2, x3)) = x2 + x3   
POL(U141(x1, x2, x3)) = x2 + x3   
POL(U15(x1, x2)) = 0   
POL(U151(x1, x2)) = x2   
POL(U16(x1)) = 0   
POL(U21(x1, x2)) = 0   
POL(U211(x1, x2)) = x2   
POL(U22(x1, x2)) = 0   
POL(U221(x1, x2)) = x2   
POL(U23(x1)) = 0   
POL(U31(x1, x2)) = 0   
POL(U311(x1, x2)) = x2   
POL(U32(x1)) = 0   
POL(U41(x1)) = 0   
POL(U51(x1, x2)) = 1 + x2   
POL(U511(x1, x2)) = x2   
POL(U52(x1, x2)) = 1 + x2   
POL(U521(x1, x2)) = x2   
POL(U61(x1, x2, x3)) = 1 + x2 + x3   
POL(U611(x1, x2, x3)) = x2 + x3   
POL(U62(x1, x2, x3)) = 1 + x2 + x3   
POL(U621(x1, x2, x3)) = x2 + x3   
POL(U63(x1, x2, x3)) = 1 + x2 + x3   
POL(U631(x1, x2, x3)) = x2 + x3   
POL(U64(x1, x2, x3)) = 1 + x2 + x3   
POL(U641(x1, x2, x3)) = x2 + x3   
POL(activate(x1)) = x1   
POL(isNat(x1)) = x1   
POL(isNatKind(x1)) = x1   
POL(n__0) = 0   
POL(n__plus(x1, x2)) = 1 + x1 + x2   
POL(n__s(x1)) = x1   
POL(plus(x1, x2)) = 1 + x1 + x2   
POL(s(x1)) = x1   
POL(tt) = 0   

The following usable rules [17] were oriented:

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



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ QDPOrderProof
QDP
              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U111(tt, V1, V2) → ACTIVATE(V2)
U111(tt, V1, V2) → ISNATKIND(activate(V1))
U211(tt, V1) → ISNATKIND(activate(V1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
U621(tt, M, N) → ACTIVATE(M)
U151(tt, V2) → ACTIVATE(V2)
U121(tt, V1, V2) → ACTIVATE(V2)
ISNATKIND(n__s(V1)) → ISNATKIND(activate(V1))
PLUS(N, s(M)) → U611(isNat(M), M, N)
U641(tt, M, N) → ACTIVATE(N)
U141(tt, V1, V2) → ACTIVATE(V1)
U611(tt, M, N) → ACTIVATE(M)
ISNAT(n__s(V1)) → ACTIVATE(V1)
U111(tt, V1, V2) → ACTIVATE(V1)
U211(tt, V1) → U221(isNatKind(activate(V1)), activate(V1))
U121(tt, V1, V2) → U131(isNatKind(activate(V2)), activate(V1), activate(V2))
U611(tt, M, N) → ACTIVATE(N)
U521(tt, N) → ACTIVATE(N)
U311(tt, V2) → ISNATKIND(activate(V2))
U141(tt, V1, V2) → ISNAT(activate(V1))
U151(tt, V2) → ISNAT(activate(V2))
U611(tt, M, N) → ISNATKIND(activate(M))
ISNAT(n__s(V1)) → U211(isNatKind(activate(V1)), activate(V1))
U141(tt, V1, V2) → U151(isNat(activate(V1)), activate(V2))
U631(tt, M, N) → U641(isNatKind(activate(N)), activate(M), activate(N))
U111(tt, V1, V2) → U121(isNatKind(activate(V1)), activate(V1), activate(V2))
U121(tt, V1, V2) → ISNATKIND(activate(V2))
U621(tt, M, N) → U631(isNat(activate(N)), activate(M), activate(N))
U611(tt, M, N) → U621(isNatKind(activate(M)), activate(M), activate(N))
ISNAT(n__s(V1)) → ISNATKIND(activate(V1))
U641(tt, M, N) → ACTIVATE(M)
U631(tt, M, N) → ACTIVATE(N)
PLUS(N, s(M)) → ISNAT(M)
U511(tt, N) → ACTIVATE(N)
U131(tt, V1, V2) → U141(isNatKind(activate(V2)), activate(V1), activate(V2))
U311(tt, V2) → ACTIVATE(V2)
ISNATKIND(n__s(V1)) → ACTIVATE(V1)
U121(tt, V1, V2) → ACTIVATE(V1)
U511(tt, N) → ISNATKIND(activate(N))
U631(tt, M, N) → ISNATKIND(activate(N))
PLUS(N, 0) → ISNAT(N)
U141(tt, V1, V2) → ACTIVATE(V2)
U621(tt, M, N) → ISNAT(activate(N))
U221(tt, V1) → ISNAT(activate(V1))
U131(tt, V1, V2) → ACTIVATE(V1)
U221(tt, V1) → ACTIVATE(V1)
U621(tt, M, N) → ACTIVATE(N)
U211(tt, V1) → ACTIVATE(V1)
U631(tt, M, N) → ACTIVATE(M)
U641(tt, M, N) → PLUS(activate(N), activate(M))
U131(tt, V1, V2) → ISNATKIND(activate(V2))
U511(tt, N) → U521(isNatKind(activate(N)), activate(N))
U131(tt, V1, V2) → ACTIVATE(V2)
PLUS(N, 0) → U511(isNat(N), N)

The TRS R consists of the following rules:

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)
0n__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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs with 44 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ QDPOrderProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
QDP
                    ↳ UsableRulesProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__s(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

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)
0n__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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ QDPOrderProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                    ↳ UsableRulesProof
QDP
                        ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__s(X)) → ACTIVATE(X)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ QDPOrderProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
QDP
                    ↳ QDPOrderProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISNATKIND(n__s(V1)) → ISNATKIND(activate(V1))

The TRS R consists of the following rules:

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)
0n__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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


ISNATKIND(n__s(V1)) → ISNATKIND(activate(V1))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(0) = 0   
POL(ISNATKIND(x1)) = x1   
POL(U11(x1, x2, x3)) = 0   
POL(U12(x1, x2, x3)) = 0   
POL(U13(x1, x2, x3)) = 0   
POL(U14(x1, x2, x3)) = 0   
POL(U15(x1, x2)) = 0   
POL(U16(x1)) = 0   
POL(U21(x1, x2)) = 0   
POL(U22(x1, x2)) = 0   
POL(U23(x1)) = 0   
POL(U31(x1, x2)) = 1   
POL(U32(x1)) = 0   
POL(U41(x1)) = 0   
POL(U51(x1, x2)) = x2   
POL(U52(x1, x2)) = x2   
POL(U61(x1, x2, x3)) = 1 + x2 + x3   
POL(U62(x1, x2, x3)) = 1 + x2 + x3   
POL(U63(x1, x2, x3)) = 1 + x2 + x3   
POL(U64(x1, x2, x3)) = 1 + x2 + x3   
POL(activate(x1)) = x1   
POL(isNat(x1)) = 0   
POL(isNatKind(x1)) = 1   
POL(n__0) = 0   
POL(n__plus(x1, x2)) = x1 + x2   
POL(n__s(x1)) = 1 + x1   
POL(plus(x1, x2)) = x1 + x2   
POL(s(x1)) = 1 + x1   
POL(tt) = 0   

The following usable rules [17] were oriented:

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



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ QDPOrderProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
QDP
                        ↳ PisEmptyProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)
0n__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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ QDPOrderProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPOrderProof
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U211(tt, V1) → U221(isNatKind(activate(V1)), activate(V1))
U221(tt, V1) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → U211(isNatKind(activate(V1)), activate(V1))

The TRS R consists of the following rules:

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)
0n__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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


ISNAT(n__s(V1)) → U211(isNatKind(activate(V1)), activate(V1))
The remaining pairs can at least be oriented weakly.

U211(tt, V1) → U221(isNatKind(activate(V1)), activate(V1))
U221(tt, V1) → ISNAT(activate(V1))
Used ordering: Polynomial interpretation [25]:

POL(0) = 1   
POL(ISNAT(x1)) = x1   
POL(U11(x1, x2, x3)) = 1   
POL(U12(x1, x2, x3)) = 1   
POL(U13(x1, x2, x3)) = 1   
POL(U14(x1, x2, x3)) = 1   
POL(U15(x1, x2)) = 1   
POL(U16(x1)) = 0   
POL(U21(x1, x2)) = 1   
POL(U211(x1, x2)) = x2   
POL(U22(x1, x2)) = 1   
POL(U221(x1, x2)) = x2   
POL(U23(x1)) = 0   
POL(U31(x1, x2)) = 0   
POL(U32(x1)) = 0   
POL(U41(x1)) = 0   
POL(U51(x1, x2)) = 1 + x2   
POL(U52(x1, x2)) = 1 + x2   
POL(U61(x1, x2, x3)) = 1 + x2 + x3   
POL(U62(x1, x2, x3)) = 1 + x2 + x3   
POL(U63(x1, x2, x3)) = 1 + x2 + x3   
POL(U64(x1, x2, x3)) = 1 + x2 + x3   
POL(activate(x1)) = x1   
POL(isNat(x1)) = 1   
POL(isNatKind(x1)) = 0   
POL(n__0) = 1   
POL(n__plus(x1, x2)) = x1 + x2   
POL(n__s(x1)) = 1 + x1   
POL(plus(x1, x2)) = x1 + x2   
POL(s(x1)) = 1 + x1   
POL(tt) = 0   

The following usable rules [17] were oriented:

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



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ QDPOrderProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
QDP
                        ↳ DependencyGraphProof
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U211(tt, V1) → U221(isNatKind(activate(V1)), activate(V1))
U221(tt, V1) → ISNAT(activate(V1))

The TRS R consists of the following rules:

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)
0n__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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ QDPOrderProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

U641(tt, M, N) → PLUS(activate(N), activate(M))
PLUS(N, s(M)) → U611(isNat(M), M, N)
U631(tt, M, N) → U641(isNatKind(activate(N)), activate(M), activate(N))
U621(tt, M, N) → U631(isNat(activate(N)), activate(M), activate(N))
U611(tt, M, N) → U621(isNatKind(activate(M)), activate(M), activate(N))

The TRS R consists of the following rules:

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)
0n__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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


U611(tt, M, N) → U621(isNatKind(activate(M)), activate(M), activate(N))
The remaining pairs can at least be oriented weakly.

U641(tt, M, N) → PLUS(activate(N), activate(M))
PLUS(N, s(M)) → U611(isNat(M), M, N)
U631(tt, M, N) → U641(isNatKind(activate(N)), activate(M), activate(N))
U621(tt, M, N) → U631(isNat(activate(N)), activate(M), activate(N))
Used ordering: Polynomial interpretation [25]:

POL(0) = 1   
POL(PLUS(x1, x2)) = x2   
POL(U11(x1, x2, x3)) = 0   
POL(U12(x1, x2, x3)) = 0   
POL(U13(x1, x2, x3)) = 0   
POL(U14(x1, x2, x3)) = 0   
POL(U15(x1, x2)) = 0   
POL(U16(x1)) = 0   
POL(U21(x1, x2)) = 0   
POL(U22(x1, x2)) = 0   
POL(U23(x1)) = 0   
POL(U31(x1, x2)) = 0   
POL(U32(x1)) = 0   
POL(U41(x1)) = 0   
POL(U51(x1, x2)) = 1 + x2   
POL(U52(x1, x2)) = 1 + x2   
POL(U61(x1, x2, x3)) = 1 + x2 + x3   
POL(U611(x1, x2, x3)) = 1 + x2   
POL(U62(x1, x2, x3)) = 1 + x2 + x3   
POL(U621(x1, x2, x3)) = x2   
POL(U63(x1, x2, x3)) = 1 + x2 + x3   
POL(U631(x1, x2, x3)) = x2   
POL(U64(x1, x2, x3)) = 1 + x2 + x3   
POL(U641(x1, x2, x3)) = x2   
POL(activate(x1)) = x1   
POL(isNat(x1)) = 0   
POL(isNatKind(x1)) = 0   
POL(n__0) = 1   
POL(n__plus(x1, x2)) = x1 + x2   
POL(n__s(x1)) = 1 + x1   
POL(plus(x1, x2)) = x1 + x2   
POL(s(x1)) = 1 + x1   
POL(tt) = 0   

The following usable rules [17] were oriented:

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



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ QDPOrderProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
QDP
                        ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U641(tt, M, N) → PLUS(activate(N), activate(M))
PLUS(N, s(M)) → U611(isNat(M), M, N)
U631(tt, M, N) → U641(isNatKind(activate(N)), activate(M), activate(N))
U621(tt, M, N) → U631(isNat(activate(N)), activate(M), activate(N))

The TRS R consists of the following rules:

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)
0n__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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 4 less nodes.