TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60044 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (9889ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (6946ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (7243ms), PolynomialLinearRange8NegiUR (timeout)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

U81#(tt, M, N) → isNatKind#(activate(M))U91#(tt, N) → activate#(N)
U34#(tt, V1, V2) → activate#(V1)U15#(tt, V2) → isNat#(activate(V2))
U32#(tt, V1, V2) → isNatKind#(activate(V2))U71#(tt, N) → U72#(isNatKind(activate(N)), activate(N))
plus#(N, 0) → U71#(isNat(N), N)U33#(tt, V1, V2) → U34#(isNatKind(activate(V2)), activate(V1), activate(V2))
isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))U103#(tt, M, N) → U104#(isNatKind(activate(N)), activate(M), activate(N))
x#(N, s(M)) → isNat#(M)U103#(tt, M, N) → isNatKind#(activate(N))
U84#(tt, M, N) → activate#(M)U32#(tt, V1, V2) → U33#(isNatKind(activate(V2)), activate(V1), activate(V2))
isNatKind#(n__x(V1, V2)) → isNatKind#(activate(V1))isNat#(n__plus(V1, V2)) → activate#(V1)
x#(N, s(M)) → U101#(isNat(M), M, N)isNatKind#(n__s(V1)) → isNatKind#(activate(V1))
U34#(tt, V1, V2) → isNat#(activate(V1))isNat#(n__s(V1)) → isNatKind#(activate(V1))
activate#(n__plus(X1, X2)) → plus#(X1, X2)isNatKind#(n__x(V1, V2)) → activate#(V1)
U82#(tt, M, N) → activate#(N)U14#(tt, V1, V2) → U15#(isNat(activate(V1)), activate(V2))
isNatKind#(n__s(V1)) → activate#(V1)U13#(tt, V1, V2) → activate#(V1)
U81#(tt, M, N) → U82#(isNatKind(activate(M)), activate(M), activate(N))isNat#(n__plus(V1, V2)) → activate#(V2)
U104#(tt, M, N) → activate#(N)plus#(N, 0) → isNat#(N)
U11#(tt, V1, V2) → activate#(V2)x#(N, 0) → isNat#(N)
U11#(tt, V1, V2) → U12#(isNatKind(activate(V1)), activate(V1), activate(V2))isNatKind#(n__plus(V1, V2)) → activate#(V2)
isNatKind#(n__x(V1, V2)) → activate#(V2)isNat#(n__x(V1, V2)) → activate#(V1)
U102#(tt, M, N) → isNat#(activate(N))isNat#(n__x(V1, V2)) → U31#(isNatKind(activate(V1)), activate(V1), activate(V2))
isNatKind#(n__plus(V1, V2)) → activate#(V1)U84#(tt, M, N) → plus#(activate(N), activate(M))
U11#(tt, V1, V2) → isNatKind#(activate(V1))U21#(tt, V1) → activate#(V1)
U35#(tt, V2) → activate#(V2)U91#(tt, N) → isNatKind#(activate(N))
U31#(tt, V1, V2) → U32#(isNatKind(activate(V1)), activate(V1), activate(V2))U103#(tt, M, N) → activate#(M)
isNat#(n__plus(V1, V2)) → U11#(isNatKind(activate(V1)), activate(V1), activate(V2))U103#(tt, M, N) → activate#(N)
U34#(tt, V1, V2) → U35#(isNat(activate(V1)), activate(V2))U83#(tt, M, N) → isNatKind#(activate(N))
U21#(tt, V1) → U22#(isNatKind(activate(V1)), activate(V1))U34#(tt, V1, V2) → activate#(V2)
U82#(tt, M, N) → U83#(isNat(activate(N)), activate(M), activate(N))U81#(tt, M, N) → activate#(M)
U104#(tt, M, N) → activate#(M)isNat#(n__x(V1, V2)) → activate#(V2)
U101#(tt, M, N) → isNatKind#(activate(M))isNatKind#(n__plus(V1, V2)) → U41#(isNatKind(activate(V1)), activate(V2))
U21#(tt, V1) → isNatKind#(activate(V1))U82#(tt, M, N) → activate#(M)
U12#(tt, V1, V2) → U13#(isNatKind(activate(V2)), activate(V1), activate(V2))U13#(tt, V1, V2) → isNatKind#(activate(V2))
isNatKind#(n__x(V1, V2)) → U61#(isNatKind(activate(V1)), activate(V2))U14#(tt, V1, V2) → isNat#(activate(V1))
U32#(tt, V1, V2) → activate#(V1)U12#(tt, V1, V2) → activate#(V1)
U12#(tt, V1, V2) → isNatKind#(activate(V2))isNat#(n__s(V1)) → activate#(V1)
U33#(tt, V1, V2) → activate#(V2)U81#(tt, M, N) → activate#(N)
plus#(N, s(M)) → U81#(isNat(M), M, N)U33#(tt, V1, V2) → activate#(V1)
U102#(tt, M, N) → activate#(N)U32#(tt, V1, V2) → activate#(V2)
U101#(tt, M, N) → U102#(isNatKind(activate(M)), activate(M), activate(N))activate#(n__x(X1, X2)) → x#(X1, X2)
U14#(tt, V1, V2) → activate#(V2)U31#(tt, V1, V2) → activate#(V2)
U15#(tt, V2) → activate#(V2)U11#(tt, V1, V2) → activate#(V1)
U104#(tt, M, N) → plus#(x(activate(N), activate(M)), activate(N))U22#(tt, V1) → activate#(V1)
U41#(tt, V2) → isNatKind#(activate(V2))U102#(tt, M, N) → activate#(M)
U102#(tt, M, N) → U103#(isNat(activate(N)), activate(M), activate(N))isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1))
U84#(tt, M, N) → activate#(N)U101#(tt, M, N) → activate#(N)
U31#(tt, V1, V2) → isNatKind#(activate(V1))U13#(tt, V1, V2) → activate#(V2)
isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))U22#(tt, V1) → isNat#(activate(V1))
isNat#(n__x(V1, V2)) → isNatKind#(activate(V1))U12#(tt, V1, V2) → activate#(V2)
U83#(tt, M, N) → activate#(N)U83#(tt, M, N) → activate#(M)
U41#(tt, V2) → activate#(V2)U13#(tt, V1, V2) → U14#(isNatKind(activate(V2)), activate(V1), activate(V2))
U33#(tt, V1, V2) → isNatKind#(activate(V2))U35#(tt, V2) → isNat#(activate(V2))
U101#(tt, M, N) → activate#(M)U61#(tt, V2) → activate#(V2)
U31#(tt, V1, V2) → activate#(V1)U83#(tt, M, N) → U84#(isNatKind(activate(N)), activate(M), activate(N))
U72#(tt, N) → activate#(N)x#(N, 0) → U91#(isNat(N), N)
U61#(tt, V2) → isNatKind#(activate(V2))U71#(tt, N) → activate#(N)
plus#(N, s(M)) → isNat#(M)U71#(tt, N) → isNatKind#(activate(N))
U82#(tt, M, N) → isNat#(activate(N))U14#(tt, V1, V2) → activate#(V1)
U104#(tt, M, N) → x#(activate(N), activate(M))

Rewrite Rules

U101(tt, M, N) → U102(isNatKind(activate(M)), activate(M), activate(N))U102(tt, M, N) → U103(isNat(activate(N)), activate(M), activate(N))
U103(tt, M, N) → U104(isNatKind(activate(N)), activate(M), activate(N))U104(tt, M, N) → plus(x(activate(N), activate(M)), activate(N))
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, V1, V2) → U32(isNatKind(activate(V1)), activate(V1), activate(V2))
U32(tt, V1, V2) → U33(isNatKind(activate(V2)), activate(V1), activate(V2))U33(tt, V1, V2) → U34(isNatKind(activate(V2)), activate(V1), activate(V2))
U34(tt, V1, V2) → U35(isNat(activate(V1)), activate(V2))U35(tt, V2) → U36(isNat(activate(V2)))
U36(tt) → ttU41(tt, V2) → U42(isNatKind(activate(V2)))
U42(tt) → ttU51(tt) → tt
U61(tt, V2) → U62(isNatKind(activate(V2)))U62(tt) → tt
U71(tt, N) → U72(isNatKind(activate(N)), activate(N))U72(tt, N) → activate(N)
U81(tt, M, N) → U82(isNatKind(activate(M)), activate(M), activate(N))U82(tt, M, N) → U83(isNat(activate(N)), activate(M), activate(N))
U83(tt, M, N) → U84(isNatKind(activate(N)), activate(M), activate(N))U84(tt, M, N) → s(plus(activate(N), activate(M)))
U91(tt, N) → U92(isNatKind(activate(N)))U92(tt) → 0
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))isNat(n__x(V1, V2)) → U31(isNatKind(activate(V1)), activate(V1), activate(V2))
isNatKind(n__0) → ttisNatKind(n__plus(V1, V2)) → U41(isNatKind(activate(V1)), activate(V2))
isNatKind(n__s(V1)) → U51(isNatKind(activate(V1)))isNatKind(n__x(V1, V2)) → U61(isNatKind(activate(V1)), activate(V2))
plus(N, 0) → U71(isNat(N), N)plus(N, s(M)) → U81(isNat(M), M, N)
x(N, 0) → U91(isNat(N), N)x(N, s(M)) → U101(isNat(M), M, N)
0 → n__0plus(X1, X2) → n__plus(X1, X2)
s(X) → n__s(X)x(X1, X2) → n__x(X1, X2)
activate(n__0) → 0activate(n__plus(X1, X2)) → plus(X1, X2)
activate(n__s(X)) → s(X)activate(n__x(X1, X2)) → x(X1, X2)
activate(X) → X

Original Signature

Termination of terms over the following signature is verified: U104, n__plus, n__s, isNat, activate, U62, n__0, U61, U42, U92, U41, U91, U23, U21, n__x, U22, plus, isNatKind, U83, U84, U71, U36, U72, 0, s, U51, U14, tt, U15, U82, U16, U81, U11, U12, U13, U31, U102, U32, U103, U33, U34, x, U101, U35

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

U81#(tt, M, N) → isNatKind#(activate(M))U91#(tt, N) → activate#(N)
U34#(tt, V1, V2) → activate#(V1)U15#(tt, V2) → isNat#(activate(V2))
U32#(tt, V1, V2) → isNatKind#(activate(V2))U71#(tt, N) → U72#(isNatKind(activate(N)), activate(N))
plus#(N, 0) → U71#(isNat(N), N)U33#(tt, V1, V2) → U34#(isNatKind(activate(V2)), activate(V1), activate(V2))
isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))U103#(tt, M, N) → U104#(isNatKind(activate(N)), activate(M), activate(N))
x#(N, s(M)) → isNat#(M)U84#(tt, M, N) → activate#(M)
U103#(tt, M, N) → isNatKind#(activate(N))isNatKind#(n__x(V1, V2)) → isNatKind#(activate(V1))
U32#(tt, V1, V2) → U33#(isNatKind(activate(V2)), activate(V1), activate(V2))isNatKind#(n__s(V1)) → U51#(isNatKind(activate(V1)))
U84#(tt, M, N) → s#(plus(activate(N), activate(M)))isNat#(n__plus(V1, V2)) → activate#(V1)
x#(N, s(M)) → U101#(isNat(M), M, N)isNatKind#(n__s(V1)) → isNatKind#(activate(V1))
U34#(tt, V1, V2) → isNat#(activate(V1))activate#(n__plus(X1, X2)) → plus#(X1, X2)
isNat#(n__s(V1)) → isNatKind#(activate(V1))isNatKind#(n__x(V1, V2)) → activate#(V1)
U82#(tt, M, N) → activate#(N)U14#(tt, V1, V2) → U15#(isNat(activate(V1)), activate(V2))
isNatKind#(n__s(V1)) → activate#(V1)U81#(tt, M, N) → U82#(isNatKind(activate(M)), activate(M), activate(N))
U13#(tt, V1, V2) → activate#(V1)isNat#(n__plus(V1, V2)) → activate#(V2)
U104#(tt, M, N) → activate#(N)plus#(N, 0) → isNat#(N)
U11#(tt, V1, V2) → activate#(V2)x#(N, 0) → isNat#(N)
U11#(tt, V1, V2) → U12#(isNatKind(activate(V1)), activate(V1), activate(V2))isNatKind#(n__plus(V1, V2)) → activate#(V2)
isNatKind#(n__x(V1, V2)) → activate#(V2)isNat#(n__x(V1, V2)) → activate#(V1)
U102#(tt, M, N) → isNat#(activate(N))isNat#(n__x(V1, V2)) → U31#(isNatKind(activate(V1)), activate(V1), activate(V2))
isNatKind#(n__plus(V1, V2)) → activate#(V1)U84#(tt, M, N) → plus#(activate(N), activate(M))
U11#(tt, V1, V2) → isNatKind#(activate(V1))U21#(tt, V1) → activate#(V1)
U91#(tt, N) → isNatKind#(activate(N))U35#(tt, V2) → activate#(V2)
U31#(tt, V1, V2) → U32#(isNatKind(activate(V1)), activate(V1), activate(V2))U103#(tt, M, N) → activate#(M)
isNat#(n__plus(V1, V2)) → U11#(isNatKind(activate(V1)), activate(V1), activate(V2))U103#(tt, M, N) → activate#(N)
U34#(tt, V1, V2) → U35#(isNat(activate(V1)), activate(V2))U83#(tt, M, N) → isNatKind#(activate(N))
U21#(tt, V1) → U22#(isNatKind(activate(V1)), activate(V1))U34#(tt, V1, V2) → activate#(V2)
U82#(tt, M, N) → U83#(isNat(activate(N)), activate(M), activate(N))U81#(tt, M, N) → activate#(M)
U104#(tt, M, N) → activate#(M)isNatKind#(n__plus(V1, V2)) → U41#(isNatKind(activate(V1)), activate(V2))
isNat#(n__x(V1, V2)) → activate#(V2)U101#(tt, M, N) → isNatKind#(activate(M))
U21#(tt, V1) → isNatKind#(activate(V1))U82#(tt, M, N) → activate#(M)
U12#(tt, V1, V2) → U13#(isNatKind(activate(V2)), activate(V1), activate(V2))U13#(tt, V1, V2) → isNatKind#(activate(V2))
isNatKind#(n__x(V1, V2)) → U61#(isNatKind(activate(V1)), activate(V2))U32#(tt, V1, V2) → activate#(V1)
U14#(tt, V1, V2) → isNat#(activate(V1))U92#(tt) → 0#
U12#(tt, V1, V2) → activate#(V1)U12#(tt, V1, V2) → isNatKind#(activate(V2))
U33#(tt, V1, V2) → activate#(V2)U81#(tt, M, N) → activate#(N)
isNat#(n__s(V1)) → activate#(V1)plus#(N, s(M)) → U81#(isNat(M), M, N)
U33#(tt, V1, V2) → activate#(V1)U32#(tt, V1, V2) → activate#(V2)
U102#(tt, M, N) → activate#(N)U101#(tt, M, N) → U102#(isNatKind(activate(M)), activate(M), activate(N))
activate#(n__x(X1, X2)) → x#(X1, X2)U14#(tt, V1, V2) → activate#(V2)
U31#(tt, V1, V2) → activate#(V2)U15#(tt, V2) → activate#(V2)
U11#(tt, V1, V2) → activate#(V1)U104#(tt, M, N) → plus#(x(activate(N), activate(M)), activate(N))
activate#(n__0) → 0#U22#(tt, V1) → activate#(V1)
U41#(tt, V2) → isNatKind#(activate(V2))U102#(tt, M, N) → activate#(M)
U35#(tt, V2) → U36#(isNat(activate(V2)))U102#(tt, M, N) → U103#(isNat(activate(N)), activate(M), activate(N))
U84#(tt, M, N) → activate#(N)isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1))
U22#(tt, V1) → U23#(isNat(activate(V1)))U101#(tt, M, N) → activate#(N)
U31#(tt, V1, V2) → isNatKind#(activate(V1))U13#(tt, V1, V2) → activate#(V2)
U61#(tt, V2) → U62#(isNatKind(activate(V2)))isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))
U22#(tt, V1) → isNat#(activate(V1))isNat#(n__x(V1, V2)) → isNatKind#(activate(V1))
U83#(tt, M, N) → activate#(N)U12#(tt, V1, V2) → activate#(V2)
U83#(tt, M, N) → activate#(M)U41#(tt, V2) → activate#(V2)
U13#(tt, V1, V2) → U14#(isNatKind(activate(V2)), activate(V1), activate(V2))U33#(tt, V1, V2) → isNatKind#(activate(V2))
U35#(tt, V2) → isNat#(activate(V2))U101#(tt, M, N) → activate#(M)
U61#(tt, V2) → activate#(V2)U31#(tt, V1, V2) → activate#(V1)
U83#(tt, M, N) → U84#(isNatKind(activate(N)), activate(M), activate(N))U91#(tt, N) → U92#(isNatKind(activate(N)))
U72#(tt, N) → activate#(N)x#(N, 0) → U91#(isNat(N), N)
U15#(tt, V2) → U16#(isNat(activate(V2)))U61#(tt, V2) → isNatKind#(activate(V2))
U71#(tt, N) → activate#(N)activate#(n__s(X)) → s#(X)
plus#(N, s(M)) → isNat#(M)U71#(tt, N) → isNatKind#(activate(N))
U82#(tt, M, N) → isNat#(activate(N))U14#(tt, V1, V2) → activate#(V1)
U104#(tt, M, N) → x#(activate(N), activate(M))U41#(tt, V2) → U42#(isNatKind(activate(V2)))

Rewrite Rules

U101(tt, M, N) → U102(isNatKind(activate(M)), activate(M), activate(N))U102(tt, M, N) → U103(isNat(activate(N)), activate(M), activate(N))
U103(tt, M, N) → U104(isNatKind(activate(N)), activate(M), activate(N))U104(tt, M, N) → plus(x(activate(N), activate(M)), activate(N))
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, V1, V2) → U32(isNatKind(activate(V1)), activate(V1), activate(V2))
U32(tt, V1, V2) → U33(isNatKind(activate(V2)), activate(V1), activate(V2))U33(tt, V1, V2) → U34(isNatKind(activate(V2)), activate(V1), activate(V2))
U34(tt, V1, V2) → U35(isNat(activate(V1)), activate(V2))U35(tt, V2) → U36(isNat(activate(V2)))
U36(tt) → ttU41(tt, V2) → U42(isNatKind(activate(V2)))
U42(tt) → ttU51(tt) → tt
U61(tt, V2) → U62(isNatKind(activate(V2)))U62(tt) → tt
U71(tt, N) → U72(isNatKind(activate(N)), activate(N))U72(tt, N) → activate(N)
U81(tt, M, N) → U82(isNatKind(activate(M)), activate(M), activate(N))U82(tt, M, N) → U83(isNat(activate(N)), activate(M), activate(N))
U83(tt, M, N) → U84(isNatKind(activate(N)), activate(M), activate(N))U84(tt, M, N) → s(plus(activate(N), activate(M)))
U91(tt, N) → U92(isNatKind(activate(N)))U92(tt) → 0
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))isNat(n__x(V1, V2)) → U31(isNatKind(activate(V1)), activate(V1), activate(V2))
isNatKind(n__0) → ttisNatKind(n__plus(V1, V2)) → U41(isNatKind(activate(V1)), activate(V2))
isNatKind(n__s(V1)) → U51(isNatKind(activate(V1)))isNatKind(n__x(V1, V2)) → U61(isNatKind(activate(V1)), activate(V2))
plus(N, 0) → U71(isNat(N), N)plus(N, s(M)) → U81(isNat(M), M, N)
x(N, 0) → U91(isNat(N), N)x(N, s(M)) → U101(isNat(M), M, N)
0 → n__0plus(X1, X2) → n__plus(X1, X2)
s(X) → n__s(X)x(X1, X2) → n__x(X1, X2)
activate(n__0) → 0activate(n__plus(X1, X2)) → plus(X1, X2)
activate(n__s(X)) → s(X)activate(n__x(X1, X2)) → x(X1, X2)
activate(X) → X

Original Signature

Termination of terms over the following signature is verified: U104, n__plus, activate, isNat, n__s, U62, U61, n__0, U42, U41, U92, U91, U23, U21, n__x, U22, plus, isNatKind, U83, U84, U71, U36, U72, 0, U14, U51, s, U15, tt, U16, U82, U81, U11, U12, U31, U13, U32, U102, U33, U103, U34, U35, U101, x

Strategy

The following SCCs where found

U81#(tt, M, N) → isNatKind#(activate(M))U91#(tt, N) → activate#(N)
U34#(tt, V1, V2) → activate#(V1)U32#(tt, V1, V2) → isNatKind#(activate(V2))
U15#(tt, V2) → isNat#(activate(V2))U71#(tt, N) → U72#(isNatKind(activate(N)), activate(N))
plus#(N, 0) → U71#(isNat(N), N)U33#(tt, V1, V2) → U34#(isNatKind(activate(V2)), activate(V1), activate(V2))
isNatKind#(n__plus(V1, V2)) → isNatKind#(activate(V1))U103#(tt, M, N) → U104#(isNatKind(activate(N)), activate(M), activate(N))
x#(N, s(M)) → isNat#(M)U84#(tt, M, N) → activate#(M)
U103#(tt, M, N) → isNatKind#(activate(N))isNatKind#(n__x(V1, V2)) → isNatKind#(activate(V1))
U32#(tt, V1, V2) → U33#(isNatKind(activate(V2)), activate(V1), activate(V2))isNat#(n__plus(V1, V2)) → activate#(V1)
x#(N, s(M)) → U101#(isNat(M), M, N)isNatKind#(n__s(V1)) → isNatKind#(activate(V1))
U34#(tt, V1, V2) → isNat#(activate(V1))activate#(n__plus(X1, X2)) → plus#(X1, X2)
isNat#(n__s(V1)) → isNatKind#(activate(V1))isNatKind#(n__x(V1, V2)) → activate#(V1)
U82#(tt, M, N) → activate#(N)U14#(tt, V1, V2) → U15#(isNat(activate(V1)), activate(V2))
isNatKind#(n__s(V1)) → activate#(V1)U81#(tt, M, N) → U82#(isNatKind(activate(M)), activate(M), activate(N))
U13#(tt, V1, V2) → activate#(V1)plus#(N, 0) → isNat#(N)
U104#(tt, M, N) → activate#(N)isNat#(n__plus(V1, V2)) → activate#(V2)
x#(N, 0) → isNat#(N)U11#(tt, V1, V2) → activate#(V2)
U11#(tt, V1, V2) → U12#(isNatKind(activate(V1)), activate(V1), activate(V2))isNatKind#(n__plus(V1, V2)) → activate#(V2)
isNatKind#(n__x(V1, V2)) → activate#(V2)isNat#(n__x(V1, V2)) → activate#(V1)
isNat#(n__x(V1, V2)) → U31#(isNatKind(activate(V1)), activate(V1), activate(V2))U102#(tt, M, N) → isNat#(activate(N))
isNatKind#(n__plus(V1, V2)) → activate#(V1)U84#(tt, M, N) → plus#(activate(N), activate(M))
U11#(tt, V1, V2) → isNatKind#(activate(V1))U21#(tt, V1) → activate#(V1)
U91#(tt, N) → isNatKind#(activate(N))U35#(tt, V2) → activate#(V2)
U31#(tt, V1, V2) → U32#(isNatKind(activate(V1)), activate(V1), activate(V2))U103#(tt, M, N) → activate#(M)
isNat#(n__plus(V1, V2)) → U11#(isNatKind(activate(V1)), activate(V1), activate(V2))U103#(tt, M, N) → activate#(N)
U34#(tt, V1, V2) → U35#(isNat(activate(V1)), activate(V2))U83#(tt, M, N) → isNatKind#(activate(N))
U21#(tt, V1) → U22#(isNatKind(activate(V1)), activate(V1))U34#(tt, V1, V2) → activate#(V2)
U82#(tt, M, N) → U83#(isNat(activate(N)), activate(M), activate(N))U81#(tt, M, N) → activate#(M)
U104#(tt, M, N) → activate#(M)isNatKind#(n__plus(V1, V2)) → U41#(isNatKind(activate(V1)), activate(V2))
U101#(tt, M, N) → isNatKind#(activate(M))isNat#(n__x(V1, V2)) → activate#(V2)
U82#(tt, M, N) → activate#(M)U21#(tt, V1) → isNatKind#(activate(V1))
U12#(tt, V1, V2) → U13#(isNatKind(activate(V2)), activate(V1), activate(V2))U13#(tt, V1, V2) → isNatKind#(activate(V2))
isNatKind#(n__x(V1, V2)) → U61#(isNatKind(activate(V1)), activate(V2))U32#(tt, V1, V2) → activate#(V1)
U14#(tt, V1, V2) → isNat#(activate(V1))U12#(tt, V1, V2) → activate#(V1)
U12#(tt, V1, V2) → isNatKind#(activate(V2))U81#(tt, M, N) → activate#(N)
U33#(tt, V1, V2) → activate#(V2)isNat#(n__s(V1)) → activate#(V1)
plus#(N, s(M)) → U81#(isNat(M), M, N)U33#(tt, V1, V2) → activate#(V1)
U32#(tt, V1, V2) → activate#(V2)U102#(tt, M, N) → activate#(N)
U101#(tt, M, N) → U102#(isNatKind(activate(M)), activate(M), activate(N))activate#(n__x(X1, X2)) → x#(X1, X2)
U14#(tt, V1, V2) → activate#(V2)U31#(tt, V1, V2) → activate#(V2)
U15#(tt, V2) → activate#(V2)U11#(tt, V1, V2) → activate#(V1)
U104#(tt, M, N) → plus#(x(activate(N), activate(M)), activate(N))U41#(tt, V2) → isNatKind#(activate(V2))
U22#(tt, V1) → activate#(V1)U102#(tt, M, N) → activate#(M)
U102#(tt, M, N) → U103#(isNat(activate(N)), activate(M), activate(N))U84#(tt, M, N) → activate#(N)
isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1))U101#(tt, M, N) → activate#(N)
U13#(tt, V1, V2) → activate#(V2)U31#(tt, V1, V2) → isNatKind#(activate(V1))
isNat#(n__plus(V1, V2)) → isNatKind#(activate(V1))U22#(tt, V1) → isNat#(activate(V1))
isNat#(n__x(V1, V2)) → isNatKind#(activate(V1))U83#(tt, M, N) → activate#(N)
U12#(tt, V1, V2) → activate#(V2)U83#(tt, M, N) → activate#(M)
U41#(tt, V2) → activate#(V2)U13#(tt, V1, V2) → U14#(isNatKind(activate(V2)), activate(V1), activate(V2))
U33#(tt, V1, V2) → isNatKind#(activate(V2))U101#(tt, M, N) → activate#(M)
U35#(tt, V2) → isNat#(activate(V2))U61#(tt, V2) → activate#(V2)
U31#(tt, V1, V2) → activate#(V1)U83#(tt, M, N) → U84#(isNatKind(activate(N)), activate(M), activate(N))
U72#(tt, N) → activate#(N)x#(N, 0) → U91#(isNat(N), N)
U61#(tt, V2) → isNatKind#(activate(V2))U71#(tt, N) → activate#(N)
plus#(N, s(M)) → isNat#(M)U71#(tt, N) → isNatKind#(activate(N))
U82#(tt, M, N) → isNat#(activate(N))U14#(tt, V1, V2) → activate#(V1)
U104#(tt, M, N) → x#(activate(N), activate(M))