YES

The TRS could be proven terminating. The proof took 44406 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (920ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (917ms).
 |    | – Problem 3 was processed with processor DependencyGraph (189ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4 (777ms).
 |    |    |    | – Problem 5 was processed with processor DependencyGraph (91ms).
 |    |    |    |    | – Problem 6 was processed with processor PolynomialLinearRange4 (495ms).
 |    |    |    |    |    | – Problem 7 was processed with processor DependencyGraph (14ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

U52#(tt, N) → activate#(N)plus#(N, 0) → U51#(isNat(N), N)
U15#(tt, V2) → isNat#(activate(V2))U21#(tt, V1) → isNatKind#(activate(V1))
U12#(tt, V1, V2) → U13#(isNatKind(activate(V2)), activate(V1), activate(V2))U64#(tt, M, N) → activate#(N)
isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))U13#(tt, V1, V2) → isNatKind#(activate(V2))
U14#(tt, V1, V2) → isNat#(activate(V1))U12#(tt, V1, V2) → activate#(V1)
U51#(tt, N) → U52#(isNatKind(activate(N)), activate(N))U12#(tt, V1, V2) → isNatKind#(activate(V2))
U63#(tt, M, N) → activate#(N)isNat#(n__s(V1)) → activate#(V1)
U64#(tt, M, N) → plus#(activate(N), activate(M))isNatKind#(n__plus(V1, V2)) → U31#(isNatKind(activate(V1)), activate(V2))
U14#(tt, V1, V2) → activate#(V2)U15#(tt, V2) → activate#(V2)
U11#(tt, V1, V2) → activate#(V1)U61#(tt, M, N) → U62#(isNatKind(activate(M)), activate(M), activate(N))
U22#(tt, V1) → activate#(V1)activate#(n__0) → 0#
isNat#(n__plus(V1, V2)) → activate#(V1)isNatKind#(n__s(V1)) → isNatKind#(activate(V1))
isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1))isNat#(n__s(V1)) → isNatKind#(activate(V1))
U22#(tt, V1) → U23#(isNat(activate(V1)))U63#(tt, M, N) → isNatKind#(activate(N))
U13#(tt, V1, V2) → activate#(V2)isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))
U22#(tt, V1) → isNat#(activate(V1))activate#(n__s(X)) → activate#(X)
activate#(n__plus(X1, X2)) → plus#(activate(X1), activate(X2))U14#(tt, V1, V2) → U15#(isNat(activate(V1)), activate(V2))
U12#(tt, V1, V2) → activate#(V2)isNatKind#(n__s(V1)) → activate#(V1)
U13#(tt, V1, V2) → activate#(V1)U51#(tt, N) → isNatKind#(activate(N))
plus#(N, 0) → isNat#(N)isNat#(n__plus(V1, V2)) → activate#(V2)
U11#(tt, V1, V2) → activate#(V2)activate#(n__plus(X1, X2)) → activate#(X2)
U62#(tt, M, N) → activate#(N)U13#(tt, V1, V2) → U14#(isNatKind(activate(V2)), activate(V1), activate(V2))
U11#(tt, V1, V2) → U12#(isNatKind(activate(V1)), activate(V1), activate(V2))isNatKind#(n__plus(V1, V2)) → activate#(V2)
U62#(tt, M, N) → activate#(M)U31#(tt, V2) → isNatKind#(activate(V2))
U64#(tt, M, N) → activate#(M)activate#(n__plus(X1, X2)) → activate#(X1)
isNatKind#(n__plus(V1, V2)) → activate#(V1)U62#(tt, M, N) → isNat#(activate(N))
U61#(tt, M, N) → activate#(N)U11#(tt, V1, V2) → isNatKind#(activate(V1))
U21#(tt, V1) → activate#(V1)U63#(tt, M, N) → U64#(isNatKind(activate(N)), activate(M), activate(N))
plus#(N, s(M)) → U61#(isNat(M), M, N)U63#(tt, M, N) → activate#(M)
U61#(tt, M, N) → isNatKind#(activate(M))U15#(tt, V2) → U16#(isNat(activate(V2)))
isNat#(n__plus(V1, V2)) → U11#(isNatKind(activate(V1)), activate(V1), activate(V2))U64#(tt, M, N) → s#(plus(activate(N), activate(M)))
U62#(tt, M, N) → U63#(isNat(activate(N)), activate(M), activate(N))U31#(tt, V2) → U32#(isNatKind(activate(V2)))
plus#(N, s(M)) → isNat#(M)U51#(tt, N) → activate#(N)
U14#(tt, V1, V2) → activate#(V1)U61#(tt, M, N) → activate#(M)
isNatKind#(n__s(V1)) → U41#(isNatKind(activate(V1)))U31#(tt, V2) → activate#(V2)
U21#(tt, V1) → U22#(isNatKind(activate(V1)), activate(V1))activate#(n__s(X)) → s#(activate(X))

Rewrite 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) → ttU31(tt, V2) → U32(isNatKind(activate(V2)))
U32(tt) → ttU41(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) → ttisNat(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__0plus(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

Original Signature

Termination of terms over the following signature is verified: n__plus, U64, activate, isNat, n__s, U63, U62, n__0, U61, U41, U23, U21, U22, plus, isNatKind, 0, U14, U51, s, U15, tt, U16, U52, U11, U12, U31, U13, U32

Strategy

The following SCCs where found

U52#(tt, N) → activate#(N)plus#(N, 0) → U51#(isNat(N), N)
U15#(tt, V2) → isNat#(activate(V2))U21#(tt, V1) → isNatKind#(activate(V1))
U12#(tt, V1, V2) → U13#(isNatKind(activate(V2)), activate(V1), activate(V2))U64#(tt, M, N) → activate#(N)
isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))U13#(tt, V1, V2) → isNatKind#(activate(V2))
U14#(tt, V1, V2) → isNat#(activate(V1))U51#(tt, N) → U52#(isNatKind(activate(N)), activate(N))
U12#(tt, V1, V2) → activate#(V1)U63#(tt, M, N) → activate#(N)
U12#(tt, V1, V2) → isNatKind#(activate(V2))isNat#(n__s(V1)) → activate#(V1)
U64#(tt, M, N) → plus#(activate(N), activate(M))isNatKind#(n__plus(V1, V2)) → U31#(isNatKind(activate(V1)), activate(V2))
U14#(tt, V1, V2) → activate#(V2)U15#(tt, V2) → activate#(V2)
U11#(tt, V1, V2) → activate#(V1)U61#(tt, M, N) → U62#(isNatKind(activate(M)), activate(M), activate(N))
U22#(tt, V1) → activate#(V1)isNat#(n__plus(V1, V2)) → activate#(V1)
isNatKind#(n__s(V1)) → isNatKind#(activate(V1))isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1))
isNat#(n__s(V1)) → isNatKind#(activate(V1))U63#(tt, M, N) → isNatKind#(activate(N))
U13#(tt, V1, V2) → activate#(V2)isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))
U22#(tt, V1) → isNat#(activate(V1))activate#(n__s(X)) → activate#(X)
activate#(n__plus(X1, X2)) → plus#(activate(X1), activate(X2))U14#(tt, V1, V2) → U15#(isNat(activate(V1)), activate(V2))
U12#(tt, V1, V2) → activate#(V2)isNatKind#(n__s(V1)) → activate#(V1)
U51#(tt, N) → isNatKind#(activate(N))U13#(tt, V1, V2) → activate#(V1)
plus#(N, 0) → isNat#(N)isNat#(n__plus(V1, V2)) → activate#(V2)
U11#(tt, V1, V2) → activate#(V2)activate#(n__plus(X1, X2)) → activate#(X2)
U62#(tt, M, N) → activate#(N)U13#(tt, V1, V2) → U14#(isNatKind(activate(V2)), activate(V1), activate(V2))
U11#(tt, V1, V2) → U12#(isNatKind(activate(V1)), activate(V1), activate(V2))isNatKind#(n__plus(V1, V2)) → activate#(V2)
U62#(tt, M, N) → activate#(M)U31#(tt, V2) → isNatKind#(activate(V2))
U64#(tt, M, N) → activate#(M)activate#(n__plus(X1, X2)) → activate#(X1)
isNatKind#(n__plus(V1, V2)) → activate#(V1)U62#(tt, M, N) → isNat#(activate(N))
U11#(tt, V1, V2) → isNatKind#(activate(V1))U61#(tt, M, N) → activate#(N)
U21#(tt, V1) → activate#(V1)plus#(N, s(M)) → U61#(isNat(M), M, N)
U63#(tt, M, N) → U64#(isNatKind(activate(N)), activate(M), activate(N))U63#(tt, M, N) → activate#(M)
U61#(tt, M, N) → isNatKind#(activate(M))isNat#(n__plus(V1, V2)) → U11#(isNatKind(activate(V1)), activate(V1), activate(V2))
U62#(tt, M, N) → U63#(isNat(activate(N)), activate(M), activate(N))plus#(N, s(M)) → isNat#(M)
U51#(tt, N) → activate#(N)U14#(tt, V1, V2) → activate#(V1)
U61#(tt, M, N) → activate#(M)U31#(tt, V2) → activate#(V2)
U21#(tt, V1) → U22#(isNatKind(activate(V1)), activate(V1))

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

U52#(tt, N) → activate#(N)plus#(N, 0) → U51#(isNat(N), N)
U15#(tt, V2) → isNat#(activate(V2))U21#(tt, V1) → isNatKind#(activate(V1))
U12#(tt, V1, V2) → U13#(isNatKind(activate(V2)), activate(V1), activate(V2))U64#(tt, M, N) → activate#(N)
isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))U13#(tt, V1, V2) → isNatKind#(activate(V2))
U14#(tt, V1, V2) → isNat#(activate(V1))U12#(tt, V1, V2) → activate#(V1)
U51#(tt, N) → U52#(isNatKind(activate(N)), activate(N))U12#(tt, V1, V2) → isNatKind#(activate(V2))
U63#(tt, M, N) → activate#(N)isNat#(n__s(V1)) → activate#(V1)
U64#(tt, M, N) → plus#(activate(N), activate(M))isNatKind#(n__plus(V1, V2)) → U31#(isNatKind(activate(V1)), activate(V2))
U14#(tt, V1, V2) → activate#(V2)U15#(tt, V2) → activate#(V2)
U11#(tt, V1, V2) → activate#(V1)U61#(tt, M, N) → U62#(isNatKind(activate(M)), activate(M), activate(N))
U22#(tt, V1) → activate#(V1)isNat#(n__plus(V1, V2)) → activate#(V1)
isNatKind#(n__s(V1)) → isNatKind#(activate(V1))isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1))
isNat#(n__s(V1)) → isNatKind#(activate(V1))U63#(tt, M, N) → isNatKind#(activate(N))
U13#(tt, V1, V2) → activate#(V2)isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))
U22#(tt, V1) → isNat#(activate(V1))activate#(n__plus(X1, X2)) → plus#(activate(X1), activate(X2))
activate#(n__s(X)) → activate#(X)U14#(tt, V1, V2) → U15#(isNat(activate(V1)), activate(V2))
U12#(tt, V1, V2) → activate#(V2)isNatKind#(n__s(V1)) → activate#(V1)
U13#(tt, V1, V2) → activate#(V1)U51#(tt, N) → isNatKind#(activate(N))
isNat#(n__plus(V1, V2)) → activate#(V2)plus#(N, 0) → isNat#(N)
U11#(tt, V1, V2) → activate#(V2)U62#(tt, M, N) → activate#(N)
activate#(n__plus(X1, X2)) → activate#(X2)U13#(tt, V1, V2) → U14#(isNatKind(activate(V2)), activate(V1), activate(V2))
U11#(tt, V1, V2) → U12#(isNatKind(activate(V1)), activate(V1), activate(V2))isNatKind#(n__plus(V1, V2)) → activate#(V2)
U62#(tt, M, N) → activate#(M)U64#(tt, M, N) → activate#(M)
U31#(tt, V2) → isNatKind#(activate(V2))activate#(n__plus(X1, X2)) → activate#(X1)
isNatKind#(n__plus(V1, V2)) → activate#(V1)U62#(tt, M, N) → isNat#(activate(N))
U11#(tt, V1, V2) → isNatKind#(activate(V1))U61#(tt, M, N) → activate#(N)
U21#(tt, V1) → activate#(V1)plus#(N, s(M)) → U61#(isNat(M), M, N)
U63#(tt, M, N) → U64#(isNatKind(activate(N)), activate(M), activate(N))U63#(tt, M, N) → activate#(M)
U61#(tt, M, N) → isNatKind#(activate(M))isNat#(n__plus(V1, V2)) → U11#(isNatKind(activate(V1)), activate(V1), activate(V2))
U62#(tt, M, N) → U63#(isNat(activate(N)), activate(M), activate(N))plus#(N, s(M)) → isNat#(M)
U51#(tt, N) → activate#(N)U14#(tt, V1, V2) → activate#(V1)
U61#(tt, M, N) → activate#(M)U31#(tt, V2) → activate#(V2)
U21#(tt, V1) → U22#(isNatKind(activate(V1)), activate(V1))

Rewrite 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) → ttU31(tt, V2) → U32(isNatKind(activate(V2)))
U32(tt) → ttU41(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) → ttisNat(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__0plus(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

Original Signature

Termination of terms over the following signature is verified: n__plus, U64, activate, isNat, n__s, U63, U62, n__0, U61, U41, U23, U21, U22, plus, isNatKind, 0, U14, U51, s, U15, tt, U16, U52, U11, U12, U31, U13, U32

Strategy

Polynomial Interpretation

Standard Usable rules

U51(tt, N) → U52(isNatKind(activate(N)), activate(N))U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1))
U31(tt, V2) → U32(isNatKind(activate(V2)))activate(n__0) → 0
U41(tt) → ttisNat(n__0) → tt
U64(tt, M, N) → s(plus(activate(N), activate(M)))isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2))
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2))s(X) → n__s(X)
U32(tt) → ttisNatKind(n__plus(V1, V2)) → U31(isNatKind(activate(V1)), activate(V2))
plus(X1, X2) → n__plus(X1, X2)plus(N, 0) → U51(isNat(N), N)
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1))U22(tt, V1) → U23(isNat(activate(V1)))
U23(tt) → ttisNatKind(n__s(V1)) → U41(isNatKind(activate(V1)))
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2))plus(N, s(M)) → U61(isNat(M), M, N)
U15(tt, V2) → U16(isNat(activate(V2)))0 → n__0
isNatKind(n__0) → ttU62(tt, M, N) → U63(isNat(activate(N)), activate(M), activate(N))
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2))U16(tt) → tt
U61(tt, M, N) → U62(isNatKind(activate(M)), activate(M), activate(N))U63(tt, M, N) → U64(isNatKind(activate(N)), activate(M), activate(N))
activate(X) → XU13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2))
activate(n__s(X)) → s(activate(X))activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
U52(tt, N) → activate(N)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

isNat#(n__s(V1)) → activate#(V1)isNatKind#(n__s(V1)) → isNatKind#(activate(V1))
isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1))isNat#(n__s(V1)) → isNatKind#(activate(V1))
activate#(n__s(X)) → activate#(X)isNatKind#(n__s(V1)) → activate#(V1)
plus#(N, s(M)) → U61#(isNat(M), M, N)plus#(N, s(M)) → isNat#(M)

Problem 3: DependencyGraph

Dependency Pair Problem

Dependency Pairs

U52#(tt, N) → activate#(N)plus#(N, 0) → U51#(isNat(N), N)
U15#(tt, V2) → isNat#(activate(V2))U21#(tt, V1) → isNatKind#(activate(V1))
U12#(tt, V1, V2) → U13#(isNatKind(activate(V2)), activate(V1), activate(V2))U64#(tt, M, N) → activate#(N)
isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))U13#(tt, V1, V2) → isNatKind#(activate(V2))
U14#(tt, V1, V2) → isNat#(activate(V1))U12#(tt, V1, V2) → activate#(V1)
U51#(tt, N) → U52#(isNatKind(activate(N)), activate(N))U12#(tt, V1, V2) → isNatKind#(activate(V2))
U63#(tt, M, N) → activate#(N)U64#(tt, M, N) → plus#(activate(N), activate(M))
isNatKind#(n__plus(V1, V2)) → U31#(isNatKind(activate(V1)), activate(V2))U14#(tt, V1, V2) → activate#(V2)
U15#(tt, V2) → activate#(V2)U11#(tt, V1, V2) → activate#(V1)
U61#(tt, M, N) → U62#(isNatKind(activate(M)), activate(M), activate(N))U22#(tt, V1) → activate#(V1)
isNat#(n__plus(V1, V2)) → activate#(V1)U63#(tt, M, N) → isNatKind#(activate(N))
U13#(tt, V1, V2) → activate#(V2)isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))
U22#(tt, V1) → isNat#(activate(V1))activate#(n__plus(X1, X2)) → plus#(activate(X1), activate(X2))
U14#(tt, V1, V2) → U15#(isNat(activate(V1)), activate(V2))U12#(tt, V1, V2) → activate#(V2)
U13#(tt, V1, V2) → activate#(V1)U51#(tt, N) → isNatKind#(activate(N))
isNat#(n__plus(V1, V2)) → activate#(V2)plus#(N, 0) → isNat#(N)
U11#(tt, V1, V2) → activate#(V2)U62#(tt, M, N) → activate#(N)
activate#(n__plus(X1, X2)) → activate#(X2)U13#(tt, V1, V2) → U14#(isNatKind(activate(V2)), activate(V1), activate(V2))
U11#(tt, V1, V2) → U12#(isNatKind(activate(V1)), activate(V1), activate(V2))isNatKind#(n__plus(V1, V2)) → activate#(V2)
U62#(tt, M, N) → activate#(M)U64#(tt, M, N) → activate#(M)
U31#(tt, V2) → isNatKind#(activate(V2))activate#(n__plus(X1, X2)) → activate#(X1)
isNatKind#(n__plus(V1, V2)) → activate#(V1)U62#(tt, M, N) → isNat#(activate(N))
U11#(tt, V1, V2) → isNatKind#(activate(V1))U61#(tt, M, N) → activate#(N)
U21#(tt, V1) → activate#(V1)U63#(tt, M, N) → U64#(isNatKind(activate(N)), activate(M), activate(N))
U63#(tt, M, N) → activate#(M)U61#(tt, M, N) → isNatKind#(activate(M))
isNat#(n__plus(V1, V2)) → U11#(isNatKind(activate(V1)), activate(V1), activate(V2))U62#(tt, M, N) → U63#(isNat(activate(N)), activate(M), activate(N))
U14#(tt, V1, V2) → activate#(V1)U51#(tt, N) → activate#(N)
U61#(tt, M, N) → activate#(M)U31#(tt, V2) → activate#(V2)
U21#(tt, V1) → U22#(isNatKind(activate(V1)), activate(V1))

Rewrite 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) → ttU31(tt, V2) → U32(isNatKind(activate(V2)))
U32(tt) → ttU41(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) → ttisNat(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__0plus(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

Original Signature

Termination of terms over the following signature is verified: n__plus, n__s, isNat, activate, U64, U63, U62, U61, n__0, U41, U23, U21, U22, plus, isNatKind, 0, U14, U51, s, U15, tt, U16, U52, U11, U12, U13, U31, U32

Strategy

The following SCCs where found

U13#(tt, V1, V2) → activate#(V2)U52#(tt, N) → activate#(N)
isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))activate#(n__plus(X1, X2)) → plus#(activate(X1), activate(X2))
U14#(tt, V1, V2) → U15#(isNat(activate(V1)), activate(V2))plus#(N, 0) → U51#(isNat(N), N)
U12#(tt, V1, V2) → activate#(V2)U15#(tt, V2) → isNat#(activate(V2))
U12#(tt, V1, V2) → U13#(isNatKind(activate(V2)), activate(V1), activate(V2))U51#(tt, N) → isNatKind#(activate(N))
U13#(tt, V1, V2) → activate#(V1)plus#(N, 0) → isNat#(N)
isNat#(n__plus(V1, V2)) → activate#(V2)U11#(tt, V1, V2) → activate#(V2)
activate#(n__plus(X1, X2)) → activate#(X2)isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))
U13#(tt, V1, V2) → isNatKind#(activate(V2))U13#(tt, V1, V2) → U14#(isNatKind(activate(V2)), activate(V1), activate(V2))
U11#(tt, V1, V2) → U12#(isNatKind(activate(V1)), activate(V1), activate(V2))U14#(tt, V1, V2) → isNat#(activate(V1))
isNatKind#(n__plus(V1, V2)) → activate#(V2)U51#(tt, N) → U52#(isNatKind(activate(N)), activate(N))
U12#(tt, V1, V2) → activate#(V1)U31#(tt, V2) → isNatKind#(activate(V2))
U12#(tt, V1, V2) → isNatKind#(activate(V2))activate#(n__plus(X1, X2)) → activate#(X1)
isNatKind#(n__plus(V1, V2)) → activate#(V1)U11#(tt, V1, V2) → isNatKind#(activate(V1))
isNatKind#(n__plus(V1, V2)) → U31#(isNatKind(activate(V1)), activate(V2))U14#(tt, V1, V2) → activate#(V2)
isNat#(n__plus(V1, V2)) → U11#(isNatKind(activate(V1)), activate(V1), activate(V2))U15#(tt, V2) → activate#(V2)
U11#(tt, V1, V2) → activate#(V1)U14#(tt, V1, V2) → activate#(V1)
U51#(tt, N) → activate#(N)U31#(tt, V2) → activate#(V2)
isNat#(n__plus(V1, V2)) → activate#(V1)

Problem 4: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

U13#(tt, V1, V2) → activate#(V2)U52#(tt, N) → activate#(N)
isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))activate#(n__plus(X1, X2)) → plus#(activate(X1), activate(X2))
U14#(tt, V1, V2) → U15#(isNat(activate(V1)), activate(V2))plus#(N, 0) → U51#(isNat(N), N)
U12#(tt, V1, V2) → activate#(V2)U15#(tt, V2) → isNat#(activate(V2))
U12#(tt, V1, V2) → U13#(isNatKind(activate(V2)), activate(V1), activate(V2))U51#(tt, N) → isNatKind#(activate(N))
U13#(tt, V1, V2) → activate#(V1)plus#(N, 0) → isNat#(N)
isNat#(n__plus(V1, V2)) → activate#(V2)U11#(tt, V1, V2) → activate#(V2)
activate#(n__plus(X1, X2)) → activate#(X2)isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))
U13#(tt, V1, V2) → U14#(isNatKind(activate(V2)), activate(V1), activate(V2))U13#(tt, V1, V2) → isNatKind#(activate(V2))
U11#(tt, V1, V2) → U12#(isNatKind(activate(V1)), activate(V1), activate(V2))U14#(tt, V1, V2) → isNat#(activate(V1))
isNatKind#(n__plus(V1, V2)) → activate#(V2)U12#(tt, V1, V2) → activate#(V1)
U51#(tt, N) → U52#(isNatKind(activate(N)), activate(N))U31#(tt, V2) → isNatKind#(activate(V2))
U12#(tt, V1, V2) → isNatKind#(activate(V2))activate#(n__plus(X1, X2)) → activate#(X1)
isNatKind#(n__plus(V1, V2)) → activate#(V1)U11#(tt, V1, V2) → isNatKind#(activate(V1))
isNatKind#(n__plus(V1, V2)) → U31#(isNatKind(activate(V1)), activate(V2))U14#(tt, V1, V2) → activate#(V2)
isNat#(n__plus(V1, V2)) → U11#(isNatKind(activate(V1)), activate(V1), activate(V2))U15#(tt, V2) → activate#(V2)
U11#(tt, V1, V2) → activate#(V1)U14#(tt, V1, V2) → activate#(V1)
U51#(tt, N) → activate#(N)U31#(tt, V2) → activate#(V2)
isNat#(n__plus(V1, V2)) → activate#(V1)

Rewrite 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) → ttU31(tt, V2) → U32(isNatKind(activate(V2)))
U32(tt) → ttU41(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) → ttisNat(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__0plus(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

Original Signature

Termination of terms over the following signature is verified: n__plus, n__s, isNat, activate, U64, U63, U62, U61, n__0, U41, U23, U21, U22, plus, isNatKind, 0, U14, U51, s, U15, tt, U16, U52, U11, U12, U13, U31, U32

Strategy

Polynomial Interpretation

Standard Usable rules

U51(tt, N) → U52(isNatKind(activate(N)), activate(N))U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1))
U31(tt, V2) → U32(isNatKind(activate(V2)))activate(n__0) → 0
U41(tt) → ttisNat(n__0) → tt
U64(tt, M, N) → s(plus(activate(N), activate(M)))isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2))
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2))s(X) → n__s(X)
U32(tt) → ttisNatKind(n__plus(V1, V2)) → U31(isNatKind(activate(V1)), activate(V2))
plus(X1, X2) → n__plus(X1, X2)plus(N, 0) → U51(isNat(N), N)
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1))U22(tt, V1) → U23(isNat(activate(V1)))
U23(tt) → ttisNatKind(n__s(V1)) → U41(isNatKind(activate(V1)))
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2))plus(N, s(M)) → U61(isNat(M), M, N)
U15(tt, V2) → U16(isNat(activate(V2)))0 → n__0
isNatKind(n__0) → ttU62(tt, M, N) → U63(isNat(activate(N)), activate(M), activate(N))
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2))U16(tt) → tt
U61(tt, M, N) → U62(isNatKind(activate(M)), activate(M), activate(N))U63(tt, M, N) → U64(isNatKind(activate(N)), activate(M), activate(N))
activate(X) → XU13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2))
activate(n__s(X)) → s(activate(X))activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
U52(tt, N) → activate(N)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

U51#(tt, N) → isNatKind#(activate(N))U51#(tt, N) → U52#(isNatKind(activate(N)), activate(N))
U51#(tt, N) → activate#(N)

Problem 5: DependencyGraph

Dependency Pair Problem

Dependency Pairs

U13#(tt, V1, V2) → activate#(V2)U52#(tt, N) → activate#(N)
isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))activate#(n__plus(X1, X2)) → plus#(activate(X1), activate(X2))
U14#(tt, V1, V2) → U15#(isNat(activate(V1)), activate(V2))U12#(tt, V1, V2) → activate#(V2)
plus#(N, 0) → U51#(isNat(N), N)U15#(tt, V2) → isNat#(activate(V2))
U12#(tt, V1, V2) → U13#(isNatKind(activate(V2)), activate(V1), activate(V2))U13#(tt, V1, V2) → activate#(V1)
isNat#(n__plus(V1, V2)) → activate#(V2)plus#(N, 0) → isNat#(N)
U11#(tt, V1, V2) → activate#(V2)activate#(n__plus(X1, X2)) → activate#(X2)
isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))U13#(tt, V1, V2) → U14#(isNatKind(activate(V2)), activate(V1), activate(V2))
U13#(tt, V1, V2) → isNatKind#(activate(V2))U11#(tt, V1, V2) → U12#(isNatKind(activate(V1)), activate(V1), activate(V2))
U14#(tt, V1, V2) → isNat#(activate(V1))isNatKind#(n__plus(V1, V2)) → activate#(V2)
U12#(tt, V1, V2) → activate#(V1)U31#(tt, V2) → isNatKind#(activate(V2))
U12#(tt, V1, V2) → isNatKind#(activate(V2))activate#(n__plus(X1, X2)) → activate#(X1)
isNatKind#(n__plus(V1, V2)) → activate#(V1)U11#(tt, V1, V2) → isNatKind#(activate(V1))
isNatKind#(n__plus(V1, V2)) → U31#(isNatKind(activate(V1)), activate(V2))U14#(tt, V1, V2) → activate#(V2)
U15#(tt, V2) → activate#(V2)isNat#(n__plus(V1, V2)) → U11#(isNatKind(activate(V1)), activate(V1), activate(V2))
U11#(tt, V1, V2) → activate#(V1)U14#(tt, V1, V2) → activate#(V1)
U31#(tt, V2) → activate#(V2)isNat#(n__plus(V1, V2)) → activate#(V1)

Rewrite 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) → ttU31(tt, V2) → U32(isNatKind(activate(V2)))
U32(tt) → ttU41(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) → ttisNat(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__0plus(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

Original Signature

Termination of terms over the following signature is verified: n__plus, U64, activate, isNat, n__s, U63, U62, n__0, U61, U41, U23, U21, U22, plus, isNatKind, 0, U14, U51, s, U15, tt, U16, U52, U11, U12, U31, U13, U32

Strategy

The following SCCs where found

U13#(tt, V1, V2) → activate#(V2)isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))
activate#(n__plus(X1, X2)) → plus#(activate(X1), activate(X2))U14#(tt, V1, V2) → U15#(isNat(activate(V1)), activate(V2))
U12#(tt, V1, V2) → activate#(V2)U15#(tt, V2) → isNat#(activate(V2))
U12#(tt, V1, V2) → U13#(isNatKind(activate(V2)), activate(V1), activate(V2))U13#(tt, V1, V2) → activate#(V1)
plus#(N, 0) → isNat#(N)isNat#(n__plus(V1, V2)) → activate#(V2)
U11#(tt, V1, V2) → activate#(V2)activate#(n__plus(X1, X2)) → activate#(X2)
isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))U13#(tt, V1, V2) → U14#(isNatKind(activate(V2)), activate(V1), activate(V2))
U13#(tt, V1, V2) → isNatKind#(activate(V2))U11#(tt, V1, V2) → U12#(isNatKind(activate(V1)), activate(V1), activate(V2))
U14#(tt, V1, V2) → isNat#(activate(V1))isNatKind#(n__plus(V1, V2)) → activate#(V2)
U12#(tt, V1, V2) → activate#(V1)U31#(tt, V2) → isNatKind#(activate(V2))
U12#(tt, V1, V2) → isNatKind#(activate(V2))activate#(n__plus(X1, X2)) → activate#(X1)
isNatKind#(n__plus(V1, V2)) → activate#(V1)U11#(tt, V1, V2) → isNatKind#(activate(V1))
isNatKind#(n__plus(V1, V2)) → U31#(isNatKind(activate(V1)), activate(V2))U14#(tt, V1, V2) → activate#(V2)
isNat#(n__plus(V1, V2)) → U11#(isNatKind(activate(V1)), activate(V1), activate(V2))U15#(tt, V2) → activate#(V2)
U11#(tt, V1, V2) → activate#(V1)U14#(tt, V1, V2) → activate#(V1)
U31#(tt, V2) → activate#(V2)isNat#(n__plus(V1, V2)) → activate#(V1)

Problem 6: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

U13#(tt, V1, V2) → activate#(V2)isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))
activate#(n__plus(X1, X2)) → plus#(activate(X1), activate(X2))U14#(tt, V1, V2) → U15#(isNat(activate(V1)), activate(V2))
U12#(tt, V1, V2) → activate#(V2)U15#(tt, V2) → isNat#(activate(V2))
U12#(tt, V1, V2) → U13#(isNatKind(activate(V2)), activate(V1), activate(V2))U13#(tt, V1, V2) → activate#(V1)
plus#(N, 0) → isNat#(N)isNat#(n__plus(V1, V2)) → activate#(V2)
U11#(tt, V1, V2) → activate#(V2)activate#(n__plus(X1, X2)) → activate#(X2)
isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))U13#(tt, V1, V2) → isNatKind#(activate(V2))
U13#(tt, V1, V2) → U14#(isNatKind(activate(V2)), activate(V1), activate(V2))U11#(tt, V1, V2) → U12#(isNatKind(activate(V1)), activate(V1), activate(V2))
U14#(tt, V1, V2) → isNat#(activate(V1))isNatKind#(n__plus(V1, V2)) → activate#(V2)
U12#(tt, V1, V2) → activate#(V1)U31#(tt, V2) → isNatKind#(activate(V2))
U12#(tt, V1, V2) → isNatKind#(activate(V2))activate#(n__plus(X1, X2)) → activate#(X1)
isNatKind#(n__plus(V1, V2)) → activate#(V1)U11#(tt, V1, V2) → isNatKind#(activate(V1))
isNatKind#(n__plus(V1, V2)) → U31#(isNatKind(activate(V1)), activate(V2))U14#(tt, V1, V2) → activate#(V2)
isNat#(n__plus(V1, V2)) → U11#(isNatKind(activate(V1)), activate(V1), activate(V2))U15#(tt, V2) → activate#(V2)
U11#(tt, V1, V2) → activate#(V1)U14#(tt, V1, V2) → activate#(V1)
U31#(tt, V2) → activate#(V2)isNat#(n__plus(V1, V2)) → activate#(V1)

Rewrite 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) → ttU31(tt, V2) → U32(isNatKind(activate(V2)))
U32(tt) → ttU41(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) → ttisNat(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__0plus(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

Original Signature

Termination of terms over the following signature is verified: n__plus, U64, activate, isNat, n__s, U63, U62, n__0, U61, U41, U23, U21, U22, plus, isNatKind, 0, U14, U51, s, U15, tt, U16, U52, U11, U12, U31, U13, U32

Strategy

Polynomial Interpretation

Standard Usable rules

U51(tt, N) → U52(isNatKind(activate(N)), activate(N))U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1))
U31(tt, V2) → U32(isNatKind(activate(V2)))activate(n__0) → 0
U41(tt) → ttisNat(n__0) → tt
U64(tt, M, N) → s(plus(activate(N), activate(M)))isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2))
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2))s(X) → n__s(X)
U32(tt) → ttisNatKind(n__plus(V1, V2)) → U31(isNatKind(activate(V1)), activate(V2))
plus(X1, X2) → n__plus(X1, X2)plus(N, 0) → U51(isNat(N), N)
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1))U22(tt, V1) → U23(isNat(activate(V1)))
U23(tt) → ttisNatKind(n__s(V1)) → U41(isNatKind(activate(V1)))
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2))plus(N, s(M)) → U61(isNat(M), M, N)
U15(tt, V2) → U16(isNat(activate(V2)))0 → n__0
isNatKind(n__0) → ttU62(tt, M, N) → U63(isNat(activate(N)), activate(M), activate(N))
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2))U16(tt) → tt
U61(tt, M, N) → U62(isNatKind(activate(M)), activate(M), activate(N))U63(tt, M, N) → U64(isNatKind(activate(N)), activate(M), activate(N))
activate(X) → XU13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2))
activate(n__s(X)) → s(activate(X))activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
U52(tt, N) → activate(N)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))activate#(n__plus(X1, X2)) → plus#(activate(X1), activate(X2))
isNat#(n__plus(V1, V2)) → activate#(V2)plus#(N, 0) → isNat#(N)
U11#(tt, V1, V2) → activate#(V2)activate#(n__plus(X1, X2)) → activate#(X2)
isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))U11#(tt, V1, V2) → U12#(isNatKind(activate(V1)), activate(V1), activate(V2))
isNatKind#(n__plus(V1, V2)) → activate#(V2)activate#(n__plus(X1, X2)) → activate#(X1)
isNatKind#(n__plus(V1, V2)) → activate#(V1)U11#(tt, V1, V2) → isNatKind#(activate(V1))
isNatKind#(n__plus(V1, V2)) → U31#(isNatKind(activate(V1)), activate(V2))isNat#(n__plus(V1, V2)) → U11#(isNatKind(activate(V1)), activate(V1), activate(V2))
U11#(tt, V1, V2) → activate#(V1)isNat#(n__plus(V1, V2)) → activate#(V1)

Problem 7: DependencyGraph

Dependency Pair Problem

Dependency Pairs

U13#(tt, V1, V2) → activate#(V2)U14#(tt, V1, V2) → U15#(isNat(activate(V1)), activate(V2))
U12#(tt, V1, V2) → activate#(V2)U14#(tt, V1, V2) → activate#(V2)
U15#(tt, V2) → isNat#(activate(V2))U15#(tt, V2) → activate#(V2)
U12#(tt, V1, V2) → U13#(isNatKind(activate(V2)), activate(V1), activate(V2))U13#(tt, V1, V2) → activate#(V1)
U13#(tt, V1, V2) → isNatKind#(activate(V2))U13#(tt, V1, V2) → U14#(isNatKind(activate(V2)), activate(V1), activate(V2))
U14#(tt, V1, V2) → activate#(V1)U14#(tt, V1, V2) → isNat#(activate(V1))
U31#(tt, V2) → activate#(V2)U12#(tt, V1, V2) → activate#(V1)
U31#(tt, V2) → isNatKind#(activate(V2))U12#(tt, V1, V2) → isNatKind#(activate(V2))

Rewrite 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) → ttU31(tt, V2) → U32(isNatKind(activate(V2)))
U32(tt) → ttU41(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) → ttisNat(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__0plus(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

Original Signature

Termination of terms over the following signature is verified: n__plus, n__s, isNat, activate, U64, U63, U62, U61, n__0, U41, U23, U21, U22, plus, isNatKind, 0, U14, U51, s, U15, tt, U16, U52, U11, U12, U13, U31, U32

Strategy

There are no SCCs!