YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (1921ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (767ms).
 |    | – Problem 6 was processed with processor DependencyGraph (107ms).
 |    |    | – Problem 8 was processed with processor PolynomialLinearRange4 (235ms).
 |    |    |    | – Problem 10 was processed with processor PolynomialLinearRange4 (238ms).
 |    |    |    |    | – Problem 12 was processed with processor DependencyGraph (28ms).
 |    |    |    |    |    | – Problem 13 was processed with processor PolynomialLinearRange4 (42ms).
 |    |    |    |    |    |    | – Problem 14 was processed with processor PolynomialLinearRange4 (79ms).
 |    |    |    |    |    |    |    | – Problem 15 was processed with processor PolynomialLinearRange4 (100ms).
 |    |    |    |    |    |    |    |    | – Problem 16 was processed with processor PolynomialLinearRange4 (35ms).
 |    |    |    |    |    |    |    |    |    | – Problem 17 was processed with processor PolynomialLinearRange4 (48ms).
 |    |    |    |    |    |    |    |    |    |    | – Problem 18 was processed with processor PolynomialLinearRange4 (26ms).
 |    |    |    |    |    |    |    |    |    |    |    | – Problem 19 was processed with processor PolynomialLinearRange4 (68ms).
 |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 20 was processed with processor ReductionPairSAT (41ms).
 |    |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 21 was processed with processor ReductionPairSAT (40ms).
 |    |    |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 22 was processed with processor ReductionPairSAT (29ms).
 |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 23 was processed with processor ReductionPairSAT (28ms).
 |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 24 was processed with processor ReductionPairSAT (33ms).
 | – Problem 3 was processed with processor SubtermCriterion (3ms).
 |    | – Problem 5 was processed with processor DependencyGraph (6ms).
 | – Problem 4 was processed with processor PolynomialLinearRange4 (125ms).
 |    | – Problem 7 was processed with processor DependencyGraph (12ms).
 |    |    | – Problem 9 was processed with processor PolynomialLinearRange4 (62ms).
 |    |    |    | – Problem 11 was processed with processor DependencyGraph (1ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

mark#(U62(X1, X2, X3)) → a__U62#(mark(X1), X2, X3)a__U31#(tt, V2) → a__U32#(a__isNatKind(V2))
a__U14#(tt, V1, V2) → a__U15#(a__isNat(V1), V2)mark#(U64(X1, X2, X3)) → a__U64#(mark(X1), X2, X3)
mark#(U22(X1, X2)) → a__U22#(mark(X1), X2)a__U13#(tt, V1, V2) → a__U14#(a__isNatKind(V2), V1, V2)
a__U62#(tt, M, N) → a__U63#(a__isNat(N), M, N)mark#(U23(X)) → a__U23#(mark(X))
a__U64#(tt, M, N) → mark#(N)mark#(U12(X1, X2, X3)) → a__U12#(mark(X1), X2, X3)
a__U63#(tt, M, N) → a__isNatKind#(N)a__plus#(N, s(M)) → a__U61#(a__isNat(M), M, N)
mark#(U31(X1, X2)) → mark#(X1)mark#(s(X)) → mark#(X)
mark#(U13(X1, X2, X3)) → mark#(X1)a__plus#(N, 0) → a__U51#(a__isNat(N), N)
a__U62#(tt, M, N) → a__isNat#(N)a__U22#(tt, V1) → a__U23#(a__isNat(V1))
mark#(plus(X1, X2)) → a__plus#(mark(X1), mark(X2))a__isNatKind#(s(V1)) → a__U41#(a__isNatKind(V1))
a__U22#(tt, V1) → a__isNat#(V1)a__U31#(tt, V2) → a__isNatKind#(V2)
a__isNatKind#(plus(V1, V2)) → a__isNatKind#(V1)a__isNat#(s(V1)) → a__isNatKind#(V1)
a__U51#(tt, N) → a__U52#(a__isNatKind(N), N)a__U51#(tt, N) → a__isNatKind#(N)
mark#(plus(X1, X2)) → mark#(X1)mark#(U15(X1, X2)) → mark#(X1)
mark#(U15(X1, X2)) → a__U15#(mark(X1), X2)a__U61#(tt, M, N) → a__isNatKind#(M)
a__U15#(tt, V2) → a__U16#(a__isNat(V2))mark#(U13(X1, X2, X3)) → a__U13#(mark(X1), X2, X3)
mark#(U63(X1, X2, X3)) → mark#(X1)a__plus#(N, 0) → a__isNat#(N)
mark#(U41(X)) → mark#(X)mark#(U41(X)) → a__U41#(mark(X))
a__U11#(tt, V1, V2) → a__isNatKind#(V1)a__U21#(tt, V1) → a__U22#(a__isNatKind(V1), V1)
mark#(U11(X1, X2, X3)) → a__U11#(mark(X1), X2, X3)a__U61#(tt, M, N) → a__U62#(a__isNatKind(M), M, N)
mark#(U11(X1, X2, X3)) → mark#(X1)a__U52#(tt, N) → mark#(N)
a__U11#(tt, V1, V2) → a__U12#(a__isNatKind(V1), V1, V2)mark#(U63(X1, X2, X3)) → a__U63#(mark(X1), X2, X3)
mark#(isNat(X)) → a__isNat#(X)mark#(U32(X)) → a__U32#(mark(X))
mark#(U61(X1, X2, X3)) → mark#(X1)mark#(U32(X)) → mark#(X)
mark#(U21(X1, X2)) → mark#(X1)mark#(U31(X1, X2)) → a__U31#(mark(X1), X2)
a__isNatKind#(s(V1)) → a__isNatKind#(V1)a__U15#(tt, V2) → a__isNat#(V2)
mark#(U51(X1, X2)) → mark#(X1)mark#(U14(X1, X2, X3)) → mark#(X1)
mark#(U16(X)) → mark#(X)mark#(U62(X1, X2, X3)) → mark#(X1)
mark#(U22(X1, X2)) → mark#(X1)mark#(U23(X)) → mark#(X)
a__U21#(tt, V1) → a__isNatKind#(V1)mark#(plus(X1, X2)) → mark#(X2)
mark#(U14(X1, X2, X3)) → a__U14#(mark(X1), X2, X3)mark#(U52(X1, X2)) → a__U52#(mark(X1), X2)
a__plus#(N, s(M)) → a__isNat#(M)mark#(U61(X1, X2, X3)) → a__U61#(mark(X1), X2, X3)
mark#(U12(X1, X2, X3)) → mark#(X1)a__U64#(tt, M, N) → a__plus#(mark(N), mark(M))
a__U14#(tt, V1, V2) → a__isNat#(V1)a__isNat#(plus(V1, V2)) → a__U11#(a__isNatKind(V1), V1, V2)
mark#(U51(X1, X2)) → a__U51#(mark(X1), X2)a__U63#(tt, M, N) → a__U64#(a__isNatKind(N), M, N)
mark#(U52(X1, X2)) → mark#(X1)a__isNatKind#(plus(V1, V2)) → a__U31#(a__isNatKind(V1), V2)
a__isNat#(s(V1)) → a__U21#(a__isNatKind(V1), V1)mark#(U21(X1, X2)) → a__U21#(mark(X1), X2)
a__isNat#(plus(V1, V2)) → a__isNatKind#(V1)a__U13#(tt, V1, V2) → a__isNatKind#(V2)
mark#(isNatKind(X)) → a__isNatKind#(X)a__U64#(tt, M, N) → mark#(M)
mark#(U16(X)) → a__U16#(mark(X))a__U12#(tt, V1, V2) → a__isNatKind#(V2)
a__U12#(tt, V1, V2) → a__U13#(a__isNatKind(V2), V1, V2)mark#(U64(X1, X2, X3)) → mark#(X1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, isNat, U64, U63, U62, U61, U41, a__U41, a__U23, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, s, U51, U14, tt, U15, a__isNat, a__U16, U16, a__U15, U52, a__U14, a__U32, a__U31, a__U13, U11, a__U12, U12, a__U11, U13, U31, a__U61, U32, a__isNatKind

Strategy

The following SCCs where found

a__isNat#(plus(V1, V2)) → a__U11#(a__isNatKind(V1), V1, V2)a__U11#(tt, V1, V2) → a__U12#(a__isNatKind(V1), V1, V2)
a__isNat#(s(V1)) → a__U21#(a__isNatKind(V1), V1)a__U22#(tt, V1) → a__isNat#(V1)
a__U14#(tt, V1, V2) → a__U15#(a__isNat(V1), V2)a__U13#(tt, V1, V2) → a__U14#(a__isNatKind(V2), V1, V2)
a__U21#(tt, V1) → a__U22#(a__isNatKind(V1), V1)a__U12#(tt, V1, V2) → a__U13#(a__isNatKind(V2), V1, V2)
a__U15#(tt, V2) → a__isNat#(V2)a__U14#(tt, V1, V2) → a__isNat#(V1)
a__isNatKind#(plus(V1, V2)) → a__U31#(a__isNatKind(V1), V2)a__U31#(tt, V2) → a__isNatKind#(V2)
a__isNatKind#(plus(V1, V2)) → a__isNatKind#(V1)a__isNatKind#(s(V1)) → a__isNatKind#(V1)
a__U52#(tt, N) → mark#(N)mark#(U63(X1, X2, X3)) → a__U63#(mark(X1), X2, X3)
mark#(U62(X1, X2, X3)) → a__U62#(mark(X1), X2, X3)mark#(U61(X1, X2, X3)) → mark#(X1)
mark#(U32(X)) → mark#(X)mark#(U64(X1, X2, X3)) → a__U64#(mark(X1), X2, X3)
mark#(U21(X1, X2)) → mark#(X1)a__U62#(tt, M, N) → a__U63#(a__isNat(N), M, N)
mark#(U51(X1, X2)) → mark#(X1)mark#(U14(X1, X2, X3)) → mark#(X1)
mark#(U16(X)) → mark#(X)mark#(U62(X1, X2, X3)) → mark#(X1)
a__U64#(tt, M, N) → mark#(N)mark#(U22(X1, X2)) → mark#(X1)
mark#(U23(X)) → mark#(X)mark#(plus(X1, X2)) → mark#(X2)
mark#(U52(X1, X2)) → a__U52#(mark(X1), X2)a__plus#(N, s(M)) → a__U61#(a__isNat(M), M, N)
mark#(U31(X1, X2)) → mark#(X1)mark#(U61(X1, X2, X3)) → a__U61#(mark(X1), X2, X3)
mark#(s(X)) → mark#(X)mark#(U12(X1, X2, X3)) → mark#(X1)
a__U64#(tt, M, N) → a__plus#(mark(N), mark(M))a__plus#(N, 0) → a__U51#(a__isNat(N), N)
mark#(U13(X1, X2, X3)) → mark#(X1)mark#(U51(X1, X2)) → a__U51#(mark(X1), X2)
a__U63#(tt, M, N) → a__U64#(a__isNatKind(N), M, N)mark#(U52(X1, X2)) → mark#(X1)
mark#(plus(X1, X2)) → a__plus#(mark(X1), mark(X2))a__U51#(tt, N) → a__U52#(a__isNatKind(N), N)
mark#(plus(X1, X2)) → mark#(X1)mark#(U15(X1, X2)) → mark#(X1)
mark#(U63(X1, X2, X3)) → mark#(X1)mark#(U41(X)) → mark#(X)
a__U64#(tt, M, N) → mark#(M)a__U61#(tt, M, N) → a__U62#(a__isNatKind(M), M, N)
mark#(U64(X1, X2, X3)) → mark#(X1)mark#(U11(X1, X2, X3)) → mark#(X1)

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

a__U52#(tt, N) → mark#(N)mark#(U63(X1, X2, X3)) → a__U63#(mark(X1), X2, X3)
mark#(U62(X1, X2, X3)) → a__U62#(mark(X1), X2, X3)mark#(U61(X1, X2, X3)) → mark#(X1)
mark#(U32(X)) → mark#(X)mark#(U64(X1, X2, X3)) → a__U64#(mark(X1), X2, X3)
mark#(U21(X1, X2)) → mark#(X1)a__U62#(tt, M, N) → a__U63#(a__isNat(N), M, N)
mark#(U51(X1, X2)) → mark#(X1)mark#(U14(X1, X2, X3)) → mark#(X1)
mark#(U16(X)) → mark#(X)mark#(U62(X1, X2, X3)) → mark#(X1)
a__U64#(tt, M, N) → mark#(N)mark#(U23(X)) → mark#(X)
mark#(U22(X1, X2)) → mark#(X1)mark#(plus(X1, X2)) → mark#(X2)
mark#(U52(X1, X2)) → a__U52#(mark(X1), X2)a__plus#(N, s(M)) → a__U61#(a__isNat(M), M, N)
mark#(U31(X1, X2)) → mark#(X1)mark#(s(X)) → mark#(X)
mark#(U61(X1, X2, X3)) → a__U61#(mark(X1), X2, X3)mark#(U12(X1, X2, X3)) → mark#(X1)
a__U64#(tt, M, N) → a__plus#(mark(N), mark(M))mark#(U13(X1, X2, X3)) → mark#(X1)
a__plus#(N, 0) → a__U51#(a__isNat(N), N)mark#(U51(X1, X2)) → a__U51#(mark(X1), X2)
a__U63#(tt, M, N) → a__U64#(a__isNatKind(N), M, N)mark#(U52(X1, X2)) → mark#(X1)
mark#(plus(X1, X2)) → a__plus#(mark(X1), mark(X2))a__U51#(tt, N) → a__U52#(a__isNatKind(N), N)
mark#(plus(X1, X2)) → mark#(X1)mark#(U15(X1, X2)) → mark#(X1)
mark#(U63(X1, X2, X3)) → mark#(X1)mark#(U41(X)) → mark#(X)
a__U64#(tt, M, N) → mark#(M)a__U61#(tt, M, N) → a__U62#(a__isNatKind(M), M, N)
mark#(U64(X1, X2, X3)) → mark#(X1)mark#(U11(X1, X2, X3)) → mark#(X1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, isNat, U64, U63, U62, U61, U41, a__U41, a__U23, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, s, U51, U14, tt, U15, a__isNat, a__U16, U16, a__U15, U52, a__U14, a__U32, a__U31, a__U13, U11, a__U12, U12, a__U11, U13, U31, a__U61, U32, a__isNatKind

Strategy

Polynomial Interpretation

Standard Usable rules

a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNatKind(X)) → a__isNatKind(X)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__isNatKind(0) → tta__U32(tt) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)mark(U41(X)) → a__U41(mark(X))
a__isNat(0) → ttmark(U32(X)) → a__U32(mark(X))
a__isNat(X) → isNat(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U23(X) → U23(X)a__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U61(X1, X2, X3) → U61(X1, X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(U23(X)) → a__U23(mark(X))a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)
mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)mark(tt) → tt
a__U41(tt) → tta__U22(X1, X2) → U22(X1, X2)
a__U15(tt, V2) → a__U16(a__isNat(V2))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U52(X1, X2)) → a__U52(mark(X1), X2)a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)
a__U41(X) → U41(X)a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)
mark(s(X)) → s(mark(X))a__U52(X1, X2) → U52(X1, X2)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)a__U32(X) → U32(X)
a__isNatKind(X) → isNatKind(X)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U16(X) → U16(X)
a__U12(X1, X2, X3) → U12(X1, X2, X3)a__U63(X1, X2, X3) → U63(X1, X2, X3)
mark(U16(X)) → a__U16(mark(X))mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)
a__U15(X1, X2) → U15(X1, X2)a__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))a__U51(X1, X2) → U51(X1, X2)
a__U52(tt, N) → mark(N)a__plus(N, 0) → a__U51(a__isNat(N), N)
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U21(X1, X2) → U21(X1, X2)
mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)mark(0) → 0
a__plus(X1, X2) → plus(X1, X2)mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)a__U23(tt) → tt
a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)mark(U51(X1, X2)) → a__U51(mark(X1), X2)
a__U16(tt) → tta__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)
a__U22(tt, V1) → a__U23(a__isNat(V1))a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)
a__U31(X1, X2) → U31(X1, X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)

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

mark#(U62(X1, X2, X3)) → a__U62#(mark(X1), X2, X3)mark#(U61(X1, X2, X3)) → mark#(X1)
mark#(U64(X1, X2, X3)) → a__U64#(mark(X1), X2, X3)mark#(U62(X1, X2, X3)) → mark#(X1)
a__U64#(tt, M, N) → mark#(N)mark#(plus(X1, X2)) → mark#(X2)
mark#(s(X)) → mark#(X)mark#(U61(X1, X2, X3)) → a__U61#(mark(X1), X2, X3)
a__U64#(tt, M, N) → a__plus#(mark(N), mark(M))mark#(plus(X1, X2)) → a__plus#(mark(X1), mark(X2))
a__U51#(tt, N) → a__U52#(a__isNatKind(N), N)mark#(plus(X1, X2)) → mark#(X1)
mark#(U63(X1, X2, X3)) → mark#(X1)a__U64#(tt, M, N) → mark#(M)
mark#(U64(X1, X2, X3)) → mark#(X1)

Problem 6: DependencyGraph

Dependency Pair Problem

Dependency Pairs

a__U52#(tt, N) → mark#(N)mark#(U51(X1, X2)) → a__U51#(mark(X1), X2)
mark#(U63(X1, X2, X3)) → a__U63#(mark(X1), X2, X3)a__U63#(tt, M, N) → a__U64#(a__isNatKind(N), M, N)
mark#(U52(X1, X2)) → mark#(X1)mark#(U32(X)) → mark#(X)
mark#(U21(X1, X2)) → mark#(X1)a__U62#(tt, M, N) → a__U63#(a__isNat(N), M, N)
mark#(U51(X1, X2)) → mark#(X1)mark#(U14(X1, X2, X3)) → mark#(X1)
mark#(U16(X)) → mark#(X)mark#(U15(X1, X2)) → mark#(X1)
mark#(U23(X)) → mark#(X)mark#(U22(X1, X2)) → mark#(X1)
mark#(U52(X1, X2)) → a__U52#(mark(X1), X2)a__plus#(N, s(M)) → a__U61#(a__isNat(M), M, N)
mark#(U41(X)) → mark#(X)mark#(U31(X1, X2)) → mark#(X1)
mark#(U12(X1, X2, X3)) → mark#(X1)a__U61#(tt, M, N) → a__U62#(a__isNatKind(M), M, N)
mark#(U11(X1, X2, X3)) → mark#(X1)a__plus#(N, 0) → a__U51#(a__isNat(N), N)
mark#(U13(X1, X2, X3)) → mark#(X1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, U64, isNat, U63, U62, U61, U41, a__U23, a__U41, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, U14, s, U51, U15, tt, U16, a__U16, a__isNat, U52, a__U15, a__U32, a__U14, U11, a__U13, a__U31, U12, a__U12, U31, U13, a__U11, U32, a__U61, a__isNatKind

Strategy

The following SCCs where found

a__U52#(tt, N) → mark#(N)mark#(U52(X1, X2)) → mark#(X1)
mark#(U32(X)) → mark#(X)mark#(U21(X1, X2)) → mark#(X1)
mark#(U51(X1, X2)) → mark#(X1)mark#(U14(X1, X2, X3)) → mark#(X1)
mark#(U16(X)) → mark#(X)mark#(U15(X1, X2)) → mark#(X1)
mark#(U22(X1, X2)) → mark#(X1)mark#(U23(X)) → mark#(X)
mark#(U52(X1, X2)) → a__U52#(mark(X1), X2)mark#(U41(X)) → mark#(X)
mark#(U31(X1, X2)) → mark#(X1)mark#(U12(X1, X2, X3)) → mark#(X1)
mark#(U11(X1, X2, X3)) → mark#(X1)mark#(U13(X1, X2, X3)) → mark#(X1)

Problem 8: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

a__U52#(tt, N) → mark#(N)mark#(U52(X1, X2)) → mark#(X1)
mark#(U32(X)) → mark#(X)mark#(U21(X1, X2)) → mark#(X1)
mark#(U51(X1, X2)) → mark#(X1)mark#(U14(X1, X2, X3)) → mark#(X1)
mark#(U16(X)) → mark#(X)mark#(U15(X1, X2)) → mark#(X1)
mark#(U23(X)) → mark#(X)mark#(U22(X1, X2)) → mark#(X1)
mark#(U52(X1, X2)) → a__U52#(mark(X1), X2)mark#(U31(X1, X2)) → mark#(X1)
mark#(U41(X)) → mark#(X)mark#(U12(X1, X2, X3)) → mark#(X1)
mark#(U11(X1, X2, X3)) → mark#(X1)mark#(U13(X1, X2, X3)) → mark#(X1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, U64, isNat, U63, U62, U61, U41, a__U23, a__U41, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, U14, s, U51, U15, tt, U16, a__U16, a__isNat, U52, a__U15, a__U32, a__U14, U11, a__U13, a__U31, U12, a__U12, U31, U13, a__U11, U32, a__U61, a__isNatKind

Strategy

Polynomial Interpretation

Standard Usable rules

a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNatKind(X)) → a__isNatKind(X)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U32(tt) → tta__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)mark(U41(X)) → a__U41(mark(X))
a__isNat(0) → ttmark(U32(X)) → a__U32(mark(X))
a__isNat(X) → isNat(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U23(X) → U23(X)a__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U61(X1, X2, X3) → U61(X1, X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(U23(X)) → a__U23(mark(X))a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)
mark(tt) → ttmark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
a__U41(tt) → tta__U22(X1, X2) → U22(X1, X2)
a__U15(tt, V2) → a__U16(a__isNat(V2))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U52(X1, X2)) → a__U52(mark(X1), X2)a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)
a__U41(X) → U41(X)a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)
mark(s(X)) → s(mark(X))a__U52(X1, X2) → U52(X1, X2)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)a__isNatKind(X) → isNatKind(X)
a__U32(X) → U32(X)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U16(X) → U16(X)
a__U12(X1, X2, X3) → U12(X1, X2, X3)a__U63(X1, X2, X3) → U63(X1, X2, X3)
mark(U16(X)) → a__U16(mark(X))mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)
a__U15(X1, X2) → U15(X1, X2)a__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))a__U51(X1, X2) → U51(X1, X2)
a__U52(tt, N) → mark(N)a__plus(N, 0) → a__U51(a__isNat(N), N)
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U21(X1, X2) → U21(X1, X2)
mark(0) → 0mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
a__plus(X1, X2) → plus(X1, X2)mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__U23(tt) → ttmark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)mark(U51(X1, X2)) → a__U51(mark(X1), X2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__U16(tt) → tt
a__U22(tt, V1) → a__U23(a__isNat(V1))a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)
a__U31(X1, X2) → U31(X1, X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)

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

mark#(U51(X1, X2)) → mark#(X1)

Problem 10: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

a__U52#(tt, N) → mark#(N)mark#(U52(X1, X2)) → mark#(X1)
mark#(U32(X)) → mark#(X)mark#(U21(X1, X2)) → mark#(X1)
mark#(U14(X1, X2, X3)) → mark#(X1)mark#(U16(X)) → mark#(X)
mark#(U15(X1, X2)) → mark#(X1)mark#(U23(X)) → mark#(X)
mark#(U22(X1, X2)) → mark#(X1)mark#(U52(X1, X2)) → a__U52#(mark(X1), X2)
mark#(U31(X1, X2)) → mark#(X1)mark#(U41(X)) → mark#(X)
mark#(U12(X1, X2, X3)) → mark#(X1)mark#(U11(X1, X2, X3)) → mark#(X1)
mark#(U13(X1, X2, X3)) → mark#(X1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, isNat, U64, U63, U62, U61, U41, a__U41, a__U23, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, U51, U14, s, tt, U15, a__isNat, a__U16, U16, a__U15, U52, a__U14, a__U32, a__U31, a__U13, U11, a__U12, U12, a__U11, U13, U31, a__U61, U32, a__isNatKind

Strategy

Polynomial Interpretation

Standard Usable rules

a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNatKind(X)) → a__isNatKind(X)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U32(tt) → tta__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)mark(U41(X)) → a__U41(mark(X))
a__isNat(0) → ttmark(U32(X)) → a__U32(mark(X))
a__isNat(X) → isNat(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U23(X) → U23(X)a__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U61(X1, X2, X3) → U61(X1, X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(U23(X)) → a__U23(mark(X))a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)
mark(tt) → ttmark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
a__U41(tt) → tta__U22(X1, X2) → U22(X1, X2)
a__U15(tt, V2) → a__U16(a__isNat(V2))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U52(X1, X2)) → a__U52(mark(X1), X2)a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)
a__U41(X) → U41(X)a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)
mark(s(X)) → s(mark(X))a__U52(X1, X2) → U52(X1, X2)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)a__isNatKind(X) → isNatKind(X)
a__U32(X) → U32(X)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U16(X) → U16(X)
a__U12(X1, X2, X3) → U12(X1, X2, X3)a__U63(X1, X2, X3) → U63(X1, X2, X3)
mark(U16(X)) → a__U16(mark(X))mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)
a__U15(X1, X2) → U15(X1, X2)a__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))a__U51(X1, X2) → U51(X1, X2)
a__U52(tt, N) → mark(N)a__plus(N, 0) → a__U51(a__isNat(N), N)
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U21(X1, X2) → U21(X1, X2)
mark(0) → 0mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
a__plus(X1, X2) → plus(X1, X2)mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__U23(tt) → ttmark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)mark(U51(X1, X2)) → a__U51(mark(X1), X2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__U16(tt) → tt
a__U22(tt, V1) → a__U23(a__isNat(V1))a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)
a__U31(X1, X2) → U31(X1, X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)

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

a__U52#(tt, N) → mark#(N)mark#(U52(X1, X2)) → mark#(X1)

Problem 12: DependencyGraph

Dependency Pair Problem

Dependency Pairs

mark#(U32(X)) → mark#(X)mark#(U21(X1, X2)) → mark#(X1)
mark#(U14(X1, X2, X3)) → mark#(X1)mark#(U16(X)) → mark#(X)
mark#(U15(X1, X2)) → mark#(X1)mark#(U23(X)) → mark#(X)
mark#(U22(X1, X2)) → mark#(X1)mark#(U52(X1, X2)) → a__U52#(mark(X1), X2)
mark#(U31(X1, X2)) → mark#(X1)mark#(U41(X)) → mark#(X)
mark#(U12(X1, X2, X3)) → mark#(X1)mark#(U11(X1, X2, X3)) → mark#(X1)
mark#(U13(X1, X2, X3)) → mark#(X1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, U64, isNat, U63, U62, U61, U41, a__U23, a__U41, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, s, U51, U14, U15, tt, U16, a__U16, a__isNat, U52, a__U15, a__U32, a__U14, U11, a__U13, a__U31, U12, a__U12, U31, U13, a__U11, U32, a__U61, a__isNatKind

Strategy

The following SCCs where found

mark#(U15(X1, X2)) → mark#(X1)mark#(U23(X)) → mark#(X)
mark#(U22(X1, X2)) → mark#(X1)mark#(U32(X)) → mark#(X)
mark#(U21(X1, X2)) → mark#(X1)mark#(U31(X1, X2)) → mark#(X1)
mark#(U41(X)) → mark#(X)mark#(U12(X1, X2, X3)) → mark#(X1)
mark#(U14(X1, X2, X3)) → mark#(X1)mark#(U11(X1, X2, X3)) → mark#(X1)
mark#(U16(X)) → mark#(X)mark#(U13(X1, X2, X3)) → mark#(X1)

Problem 13: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

mark#(U15(X1, X2)) → mark#(X1)mark#(U23(X)) → mark#(X)
mark#(U22(X1, X2)) → mark#(X1)mark#(U32(X)) → mark#(X)
mark#(U31(X1, X2)) → mark#(X1)mark#(U41(X)) → mark#(X)
mark#(U21(X1, X2)) → mark#(X1)mark#(U12(X1, X2, X3)) → mark#(X1)
mark#(U14(X1, X2, X3)) → mark#(X1)mark#(U11(X1, X2, X3)) → mark#(X1)
mark#(U16(X)) → mark#(X)mark#(U13(X1, X2, X3)) → mark#(X1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, U64, isNat, U63, U62, U61, U41, a__U23, a__U41, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, s, U51, U14, U15, tt, U16, a__U16, a__isNat, U52, a__U15, a__U32, a__U14, U11, a__U13, a__U31, U12, a__U12, U31, U13, a__U11, U32, a__U61, a__isNatKind

Strategy

Polynomial Interpretation

There are no usable rules

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

mark#(U14(X1, X2, X3)) → mark#(X1)

Problem 14: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

mark#(U15(X1, X2)) → mark#(X1)mark#(U22(X1, X2)) → mark#(X1)
mark#(U23(X)) → mark#(X)mark#(U32(X)) → mark#(X)
mark#(U21(X1, X2)) → mark#(X1)mark#(U41(X)) → mark#(X)
mark#(U31(X1, X2)) → mark#(X1)mark#(U12(X1, X2, X3)) → mark#(X1)
mark#(U16(X)) → mark#(X)mark#(U11(X1, X2, X3)) → mark#(X1)
mark#(U13(X1, X2, X3)) → mark#(X1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, isNat, U64, U63, U62, U61, U41, a__U41, a__U23, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, U14, s, U51, tt, U15, a__isNat, a__U16, U16, a__U15, U52, a__U14, a__U32, a__U31, a__U13, U11, a__U12, U12, a__U11, U13, U31, a__U61, U32, a__isNatKind

Strategy

Polynomial Interpretation

There are no usable rules

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

mark#(U41(X)) → mark#(X)

Problem 15: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

mark#(U15(X1, X2)) → mark#(X1)mark#(U23(X)) → mark#(X)
mark#(U22(X1, X2)) → mark#(X1)mark#(U32(X)) → mark#(X)
mark#(U31(X1, X2)) → mark#(X1)mark#(U21(X1, X2)) → mark#(X1)
mark#(U12(X1, X2, X3)) → mark#(X1)mark#(U11(X1, X2, X3)) → mark#(X1)
mark#(U16(X)) → mark#(X)mark#(U13(X1, X2, X3)) → mark#(X1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, U64, isNat, U63, U62, U61, U41, a__U23, a__U41, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, U51, U14, s, U15, tt, U16, a__U16, a__isNat, U52, a__U15, a__U32, a__U14, U11, a__U13, a__U31, U12, a__U12, U31, U13, a__U11, U32, a__U61, a__isNatKind

Strategy

Polynomial Interpretation

There are no usable rules

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

mark#(U21(X1, X2)) → mark#(X1)

Problem 16: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

mark#(U15(X1, X2)) → mark#(X1)mark#(U22(X1, X2)) → mark#(X1)
mark#(U23(X)) → mark#(X)mark#(U32(X)) → mark#(X)
mark#(U31(X1, X2)) → mark#(X1)mark#(U12(X1, X2, X3)) → mark#(X1)
mark#(U16(X)) → mark#(X)mark#(U11(X1, X2, X3)) → mark#(X1)
mark#(U13(X1, X2, X3)) → mark#(X1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, isNat, U64, U63, U62, U61, U41, a__U41, a__U23, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, s, U51, U14, tt, U15, a__isNat, a__U16, U16, a__U15, U52, a__U14, a__U32, a__U31, a__U13, U11, a__U12, U12, a__U11, U13, U31, a__U61, U32, a__isNatKind

Strategy

Polynomial Interpretation

There are no usable rules

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

mark#(U23(X)) → mark#(X)

Problem 17: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

mark#(U15(X1, X2)) → mark#(X1)mark#(U22(X1, X2)) → mark#(X1)
mark#(U32(X)) → mark#(X)mark#(U31(X1, X2)) → mark#(X1)
mark#(U12(X1, X2, X3)) → mark#(X1)mark#(U11(X1, X2, X3)) → mark#(X1)
mark#(U16(X)) → mark#(X)mark#(U13(X1, X2, X3)) → mark#(X1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, U64, isNat, U63, U62, U61, U41, a__U23, a__U41, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, U14, s, U51, U15, tt, U16, a__U16, a__isNat, U52, a__U15, a__U32, a__U14, U11, a__U13, a__U31, U12, a__U12, U31, U13, a__U11, U32, a__U61, a__isNatKind

Strategy

Polynomial Interpretation

There are no usable rules

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

mark#(U31(X1, X2)) → mark#(X1)

Problem 18: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

mark#(U15(X1, X2)) → mark#(X1)mark#(U22(X1, X2)) → mark#(X1)
mark#(U32(X)) → mark#(X)mark#(U12(X1, X2, X3)) → mark#(X1)
mark#(U16(X)) → mark#(X)mark#(U11(X1, X2, X3)) → mark#(X1)
mark#(U13(X1, X2, X3)) → mark#(X1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, isNat, U64, U63, U62, U61, U41, a__U41, a__U23, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, U51, U14, s, tt, U15, a__isNat, a__U16, U16, a__U15, U52, a__U14, a__U32, a__U31, a__U13, U11, a__U12, U12, a__U11, U13, U31, a__U61, U32, a__isNatKind

Strategy

Polynomial Interpretation

There are no usable rules

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

mark#(U11(X1, X2, X3)) → mark#(X1)

Problem 19: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

mark#(U15(X1, X2)) → mark#(X1)mark#(U22(X1, X2)) → mark#(X1)
mark#(U32(X)) → mark#(X)mark#(U12(X1, X2, X3)) → mark#(X1)
mark#(U16(X)) → mark#(X)mark#(U13(X1, X2, X3)) → mark#(X1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, U64, isNat, U63, U62, U61, U41, a__U23, a__U41, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, s, U51, U14, U15, tt, U16, a__U16, a__isNat, U52, a__U15, a__U32, a__U14, U11, a__U13, a__U31, U12, a__U12, U31, U13, a__U11, U32, a__U61, a__isNatKind

Strategy

Polynomial Interpretation

There are no usable rules

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

mark#(U15(X1, X2)) → mark#(X1)

Problem 20: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

mark#(U22(X1, X2)) → mark#(X1)mark#(U32(X)) → mark#(X)
mark#(U12(X1, X2, X3)) → mark#(X1)mark#(U16(X)) → mark#(X)
mark#(U13(X1, X2, X3)) → mark#(X1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, isNat, U64, U63, U62, U61, U41, a__U41, a__U23, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, U14, s, U51, tt, U15, a__isNat, a__U16, U16, a__U15, U52, a__U14, a__U32, a__U31, a__U13, U11, a__U12, U12, a__U11, U13, U31, a__U61, U32, a__isNatKind

Strategy

Function Precedence

U22 = U16 = U32 < a__U51 = a__U52 = U64 = isNat = U63 = U62 = U61 = U41 = a__U23 = a__U41 = a__U22 = U23 = U21 = a__U21 = a__U64 = plus = a__U62 = a__U63 = isNatKind = a__plus = mark = mark# = 0 = s = U14 = U51 = U15 = tt = a__U16 = a__isNat = U52 = a__U15 = a__U32 = a__U14 = U11 = a__U31 = a__U13 = a__U12 = U12 = U31 = U13 = a__U11 = a__U61 = a__isNatKind

Argument Filtering

a__U51: all arguments are removed from a__U51
a__U52: all arguments are removed from a__U52
U64: all arguments are removed from U64
isNat: all arguments are removed from isNat
U63: 1 2
U62: all arguments are removed from U62
U61: 1 2 3
U41: all arguments are removed from U41
a__U23: all arguments are removed from a__U23
a__U41: all arguments are removed from a__U41
a__U22: all arguments are removed from a__U22
U23: all arguments are removed from U23
U21: all arguments are removed from U21
a__U21: all arguments are removed from a__U21
U22: collapses to 1
a__U64: all arguments are removed from a__U64
plus: all arguments are removed from plus
a__U62: all arguments are removed from a__U62
a__U63: all arguments are removed from a__U63
isNatKind: all arguments are removed from isNatKind
a__plus: all arguments are removed from a__plus
mark: all arguments are removed from mark
mark#: collapses to 1
0: all arguments are removed from 0
s: all arguments are removed from s
U14: all arguments are removed from U14
U51: all arguments are removed from U51
U15: all arguments are removed from U15
tt: all arguments are removed from tt
a__U16: collapses to 1
U16: collapses to 1
a__isNat: all arguments are removed from a__isNat
U52: all arguments are removed from U52
a__U15: all arguments are removed from a__U15
a__U32: all arguments are removed from a__U32
a__U14: all arguments are removed from a__U14
U11: all arguments are removed from U11
a__U31: all arguments are removed from a__U31
a__U13: all arguments are removed from a__U13
a__U12: all arguments are removed from a__U12
U12: collapses to 1
U31: all arguments are removed from U31
U13: 1
a__U11: all arguments are removed from a__U11
U32: collapses to 1
a__U61: all arguments are removed from a__U61
a__isNatKind: all arguments are removed from a__isNatKind

Status

a__U51: multiset
a__U52: multiset
U64: multiset
isNat: multiset
U63: lexicographic with permutation 1 → 1 2 → 2
U62: multiset
U61: lexicographic with permutation 1 → 3 2 → 1 3 → 2
U41: multiset
a__U23: multiset
a__U41: multiset
a__U22: multiset
U23: multiset
U21: multiset
a__U21: multiset
a__U64: multiset
plus: multiset
a__U62: multiset
a__U63: multiset
isNatKind: multiset
a__plus: multiset
mark: multiset
0: multiset
s: multiset
U14: multiset
U51: multiset
U15: multiset
tt: multiset
a__isNat: multiset
U52: multiset
a__U15: multiset
a__U32: multiset
a__U14: multiset
U11: multiset
a__U31: multiset
a__U13: multiset
a__U12: multiset
U31: multiset
U13: multiset
a__U11: multiset
a__U61: multiset
a__isNatKind: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

mark#(U13(X1, X2, X3)) → mark#(X1)

Problem 21: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

mark#(U22(X1, X2)) → mark#(X1)mark#(U32(X)) → mark#(X)
mark#(U12(X1, X2, X3)) → mark#(X1)mark#(U16(X)) → mark#(X)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, U64, isNat, U63, U62, U61, U41, a__U23, a__U41, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, U51, U14, s, U15, tt, U16, a__U16, a__isNat, U52, a__U15, a__U32, a__U14, U11, a__U13, a__U31, U12, a__U12, U31, U13, a__U11, U32, a__U61, a__isNatKind

Strategy

Function Precedence

U16 = U12 = U32 < U22 < a__U51 = a__U52 = U64 = isNat = U63 = U62 = U61 = U41 = a__U23 = a__U41 = a__U22 = U23 = U21 = a__U21 = a__U64 = plus = a__U62 = a__U63 = isNatKind = a__plus = mark = mark# = 0 = s = U14 = U51 = U15 = tt = a__U16 = a__isNat = U52 = a__U15 = a__U32 = a__U14 = U11 = a__U31 = a__U13 = a__U12 = U31 = U13 = a__U11 = a__U61 = a__isNatKind

Argument Filtering

a__U51: all arguments are removed from a__U51
a__U52: all arguments are removed from a__U52
U64: all arguments are removed from U64
isNat: all arguments are removed from isNat
U63: all arguments are removed from U63
U62: all arguments are removed from U62
U61: all arguments are removed from U61
U41: all arguments are removed from U41
a__U23: all arguments are removed from a__U23
a__U41: all arguments are removed from a__U41
a__U22: all arguments are removed from a__U22
U23: all arguments are removed from U23
U21: all arguments are removed from U21
a__U21: all arguments are removed from a__U21
U22: 1
a__U64: all arguments are removed from a__U64
plus: all arguments are removed from plus
a__U62: all arguments are removed from a__U62
a__U63: all arguments are removed from a__U63
isNatKind: all arguments are removed from isNatKind
a__plus: all arguments are removed from a__plus
mark: all arguments are removed from mark
mark#: collapses to 1
0: all arguments are removed from 0
s: all arguments are removed from s
U14: all arguments are removed from U14
U51: all arguments are removed from U51
U15: all arguments are removed from U15
tt: all arguments are removed from tt
a__U16: all arguments are removed from a__U16
U16: collapses to 1
a__isNat: all arguments are removed from a__isNat
U52: all arguments are removed from U52
a__U15: all arguments are removed from a__U15
a__U32: all arguments are removed from a__U32
a__U14: 2
U11: all arguments are removed from U11
a__U31: all arguments are removed from a__U31
a__U13: all arguments are removed from a__U13
a__U12: all arguments are removed from a__U12
U12: collapses to 1
U31: all arguments are removed from U31
U13: all arguments are removed from U13
a__U11: all arguments are removed from a__U11
U32: collapses to 1
a__U61: all arguments are removed from a__U61
a__isNatKind: all arguments are removed from a__isNatKind

Status

a__U51: multiset
a__U52: multiset
U64: multiset
isNat: multiset
U63: multiset
U62: multiset
U61: multiset
U41: multiset
a__U23: multiset
a__U41: multiset
a__U22: multiset
U23: multiset
U21: multiset
a__U21: multiset
U22: multiset
a__U64: multiset
plus: multiset
a__U62: multiset
a__U63: multiset
isNatKind: multiset
a__plus: multiset
mark: multiset
0: multiset
s: multiset
U14: multiset
U51: multiset
U15: multiset
tt: multiset
a__U16: multiset
a__isNat: multiset
U52: multiset
a__U15: multiset
a__U32: multiset
a__U14: lexicographic with permutation 2 → 1
U11: multiset
a__U31: multiset
a__U13: multiset
a__U12: multiset
U31: multiset
U13: multiset
a__U11: multiset
a__U61: multiset
a__isNatKind: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

mark#(U22(X1, X2)) → mark#(X1)

Problem 22: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

mark#(U32(X)) → mark#(X)mark#(U12(X1, X2, X3)) → mark#(X1)
mark#(U16(X)) → mark#(X)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, isNat, U64, U63, U62, U61, U41, a__U41, a__U23, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, s, U51, U14, tt, U15, a__isNat, a__U16, U16, a__U15, U52, a__U14, a__U32, a__U31, a__U13, U11, a__U12, U12, a__U11, U13, U31, a__U61, U32, a__isNatKind

Strategy

Function Precedence

U16 = U12 < U32 < a__U51 = a__U52 = U64 = isNat = U63 = U62 = U61 = U41 = a__U23 = a__U41 = a__U22 = U23 = U21 = a__U21 = U22 = a__U64 = plus = a__U62 = a__U63 = isNatKind = a__plus = mark = mark# = 0 = s = U14 = U51 = U15 = tt = a__U16 = a__isNat = U52 = a__U15 = a__U32 = a__U14 = U11 = a__U31 = a__U13 = a__U12 = U31 = U13 = a__U11 = a__U61 = a__isNatKind

Argument Filtering

a__U51: all arguments are removed from a__U51
a__U52: all arguments are removed from a__U52
U64: all arguments are removed from U64
isNat: all arguments are removed from isNat
U63: collapses to 2
U62: all arguments are removed from U62
U61: all arguments are removed from U61
U41: all arguments are removed from U41
a__U23: all arguments are removed from a__U23
a__U41: all arguments are removed from a__U41
a__U22: all arguments are removed from a__U22
U23: all arguments are removed from U23
U21: all arguments are removed from U21
a__U21: all arguments are removed from a__U21
U22: all arguments are removed from U22
a__U64: all arguments are removed from a__U64
plus: 1 2
a__U62: all arguments are removed from a__U62
a__U63: all arguments are removed from a__U63
isNatKind: all arguments are removed from isNatKind
a__plus: all arguments are removed from a__plus
mark: all arguments are removed from mark
mark#: collapses to 1
0: all arguments are removed from 0
s: all arguments are removed from s
U14: all arguments are removed from U14
U51: all arguments are removed from U51
U15: all arguments are removed from U15
tt: all arguments are removed from tt
a__U16: all arguments are removed from a__U16
U16: collapses to 1
a__isNat: all arguments are removed from a__isNat
U52: all arguments are removed from U52
a__U15: all arguments are removed from a__U15
a__U32: all arguments are removed from a__U32
a__U14: all arguments are removed from a__U14
U11: all arguments are removed from U11
a__U31: all arguments are removed from a__U31
a__U13: all arguments are removed from a__U13
a__U12: all arguments are removed from a__U12
U12: collapses to 1
U31: all arguments are removed from U31
U13: all arguments are removed from U13
a__U11: all arguments are removed from a__U11
U32: 1
a__U61: all arguments are removed from a__U61
a__isNatKind: all arguments are removed from a__isNatKind

Status

a__U51: multiset
a__U52: multiset
U64: multiset
isNat: multiset
U62: multiset
U61: multiset
U41: multiset
a__U23: multiset
a__U41: multiset
a__U22: multiset
U23: multiset
U21: multiset
a__U21: multiset
U22: multiset
a__U64: multiset
plus: lexicographic with permutation 1 → 1 2 → 2
a__U62: multiset
a__U63: multiset
isNatKind: multiset
a__plus: multiset
mark: multiset
0: multiset
s: multiset
U14: multiset
U51: multiset
U15: multiset
tt: multiset
a__U16: multiset
a__isNat: multiset
U52: multiset
a__U15: multiset
a__U32: multiset
a__U14: multiset
U11: multiset
a__U31: multiset
a__U13: multiset
a__U12: multiset
U31: multiset
U13: multiset
a__U11: multiset
U32: lexicographic with permutation 1 → 1
a__U61: multiset
a__isNatKind: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

mark#(U32(X)) → mark#(X)

Problem 23: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

mark#(U12(X1, X2, X3)) → mark#(X1)mark#(U16(X)) → mark#(X)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, U64, isNat, U63, U62, U61, U41, a__U23, a__U41, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, U14, s, U51, U15, tt, U16, a__U16, a__isNat, U52, a__U15, a__U32, a__U14, U11, a__U13, a__U31, U12, a__U12, U31, U13, a__U11, U32, a__U61, a__isNatKind

Strategy

Function Precedence

U12 < U16 < a__U51 = a__U52 = U64 = isNat = U63 = U62 = U61 = U41 = a__U23 = a__U41 = a__U22 = U23 = U21 = a__U21 = U22 = a__U64 = plus = a__U62 = a__U63 = isNatKind = a__plus = mark = mark# = 0 = s = U14 = U51 = U15 = tt = a__U16 = a__isNat = U52 = a__U15 = a__U32 = a__U14 = U11 = a__U31 = a__U13 = a__U12 = U31 = U13 = a__U11 = U32 = a__U61 = a__isNatKind

Argument Filtering

a__U51: 1 2
a__U52: all arguments are removed from a__U52
U64: 1
isNat: all arguments are removed from isNat
U63: all arguments are removed from U63
U62: all arguments are removed from U62
U61: 1 3
U41: all arguments are removed from U41
a__U23: all arguments are removed from a__U23
a__U41: all arguments are removed from a__U41
a__U22: all arguments are removed from a__U22
U23: all arguments are removed from U23
U21: all arguments are removed from U21
a__U21: all arguments are removed from a__U21
U22: all arguments are removed from U22
a__U64: all arguments are removed from a__U64
plus: 1 2
a__U62: all arguments are removed from a__U62
a__U63: all arguments are removed from a__U63
isNatKind: all arguments are removed from isNatKind
a__plus: all arguments are removed from a__plus
mark: all arguments are removed from mark
mark#: collapses to 1
0: all arguments are removed from 0
s: all arguments are removed from s
U14: all arguments are removed from U14
U51: 1 2
U15: all arguments are removed from U15
tt: all arguments are removed from tt
a__U16: all arguments are removed from a__U16
U16: 1
a__isNat: all arguments are removed from a__isNat
U52: 1 2
a__U15: all arguments are removed from a__U15
a__U32: all arguments are removed from a__U32
a__U14: all arguments are removed from a__U14
U11: all arguments are removed from U11
a__U31: all arguments are removed from a__U31
a__U13: all arguments are removed from a__U13
a__U12: all arguments are removed from a__U12
U12: collapses to 1
U31: all arguments are removed from U31
U13: all arguments are removed from U13
a__U11: all arguments are removed from a__U11
U32: 1
a__U61: all arguments are removed from a__U61
a__isNatKind: all arguments are removed from a__isNatKind

Status

a__U51: lexicographic with permutation 1 → 2 2 → 1
a__U52: multiset
U64: lexicographic with permutation 1 → 1
isNat: multiset
U63: multiset
U62: multiset
U61: lexicographic with permutation 1 → 1 3 → 2
U41: multiset
a__U23: multiset
a__U41: multiset
a__U22: multiset
U23: multiset
U21: multiset
a__U21: multiset
U22: multiset
a__U64: multiset
plus: lexicographic with permutation 1 → 1 2 → 2
a__U62: multiset
a__U63: multiset
isNatKind: multiset
a__plus: multiset
mark: multiset
0: multiset
s: multiset
U14: multiset
U51: lexicographic with permutation 1 → 2 2 → 1
U15: multiset
tt: multiset
a__U16: multiset
U16: multiset
a__isNat: multiset
U52: lexicographic with permutation 1 → 2 2 → 1
a__U15: multiset
a__U32: multiset
a__U14: multiset
U11: multiset
a__U31: multiset
a__U13: multiset
a__U12: multiset
U31: multiset
U13: multiset
a__U11: multiset
U32: lexicographic with permutation 1 → 1
a__U61: multiset
a__isNatKind: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

mark#(U16(X)) → mark#(X)

Problem 24: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

mark#(U12(X1, X2, X3)) → mark#(X1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, isNat, U64, U63, U62, U61, U41, a__U41, a__U23, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, U51, U14, s, tt, U15, a__isNat, a__U16, U16, a__U15, U52, a__U14, a__U32, a__U31, a__U13, U11, a__U12, U12, a__U11, U13, U31, a__U61, U32, a__isNatKind

Strategy

Function Precedence

mark# < U12 < a__U51 = a__U52 = U64 = isNat = U63 = U62 = U61 = U41 = a__U23 = a__U41 = a__U22 = U23 = U21 = a__U21 = U22 = a__U64 = plus = a__U62 = a__U63 = isNatKind = a__plus = mark = 0 = s = U14 = U51 = U15 = tt = a__U16 = U16 = a__isNat = U52 = a__U15 = a__U32 = a__U14 = U11 = a__U31 = a__U13 = a__U12 = U31 = U13 = a__U11 = U32 = a__U61 = a__isNatKind

Argument Filtering

a__U51: 2
a__U52: 1 2
U64: all arguments are removed from U64
isNat: all arguments are removed from isNat
U63: collapses to 1
U62: 1 3
U61: all arguments are removed from U61
U41: all arguments are removed from U41
a__U23: 1
a__U41: all arguments are removed from a__U41
a__U22: all arguments are removed from a__U22
U23: 1
U21: all arguments are removed from U21
a__U21: 2
U22: all arguments are removed from U22
a__U64: all arguments are removed from a__U64
plus: all arguments are removed from plus
a__U62: all arguments are removed from a__U62
a__U63: all arguments are removed from a__U63
isNatKind: all arguments are removed from isNatKind
a__plus: all arguments are removed from a__plus
mark: collapses to 1
mark#: 1
0: all arguments are removed from 0
s: collapses to 1
U14: 1
U51: 2
U15: all arguments are removed from U15
tt: all arguments are removed from tt
a__U16: collapses to 1
U16: collapses to 1
a__isNat: all arguments are removed from a__isNat
U52: 1 2
a__U15: 2
a__U32: collapses to 1
a__U14: all arguments are removed from a__U14
U11: all arguments are removed from U11
a__U31: 1 2
a__U13: 1 3
a__U12: all arguments are removed from a__U12
U12: 1 2
U31: all arguments are removed from U31
U13: all arguments are removed from U13
a__U11: all arguments are removed from a__U11
U32: all arguments are removed from U32
a__U61: 2 3
a__isNatKind: all arguments are removed from a__isNatKind

Status

a__U51: lexicographic with permutation 2 → 1
a__U52: lexicographic with permutation 1 → 2 2 → 1
U64: multiset
isNat: multiset
U62: lexicographic with permutation 1 → 2 3 → 1
U61: multiset
U41: multiset
a__U23: lexicographic with permutation 1 → 1
a__U41: multiset
a__U22: multiset
U23: lexicographic with permutation 1 → 1
U21: multiset
a__U21: lexicographic with permutation 2 → 1
U22: multiset
a__U64: multiset
plus: multiset
a__U62: multiset
a__U63: multiset
isNatKind: multiset
a__plus: multiset
mark#: lexicographic with permutation 1 → 1
0: multiset
U14: lexicographic with permutation 1 → 1
U51: lexicographic with permutation 2 → 1
U15: multiset
tt: multiset
a__isNat: multiset
U52: lexicographic with permutation 1 → 1 2 → 2
a__U15: lexicographic with permutation 2 → 1
a__U14: multiset
U11: multiset
a__U31: lexicographic with permutation 1 → 2 2 → 1
a__U13: lexicographic with permutation 1 → 2 3 → 1
a__U12: multiset
U12: multiset
U31: multiset
U13: multiset
a__U11: multiset
U32: multiset
a__U61: lexicographic with permutation 2 → 1 3 → 2
a__isNatKind: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

mark#(U12(X1, X2, X3)) → mark#(X1)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

a__isNatKind#(plus(V1, V2)) → a__U31#(a__isNatKind(V1), V2)a__U31#(tt, V2) → a__isNatKind#(V2)
a__isNatKind#(plus(V1, V2)) → a__isNatKind#(V1)a__isNatKind#(s(V1)) → a__isNatKind#(V1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, isNat, U64, U63, U62, U61, U41, a__U41, a__U23, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, s, U51, U14, tt, U15, a__isNat, a__U16, U16, a__U15, U52, a__U14, a__U32, a__U31, a__U13, U11, a__U12, U12, a__U11, U13, U31, a__U61, U32, a__isNatKind

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

a__isNatKind#(plus(V1, V2)) → a__U31#(a__isNatKind(V1), V2)a__isNatKind#(plus(V1, V2)) → a__isNatKind#(V1)
a__isNatKind#(s(V1)) → a__isNatKind#(V1)

Problem 5: DependencyGraph

Dependency Pair Problem

Dependency Pairs

a__U31#(tt, V2) → a__isNatKind#(V2)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, U64, isNat, U63, U62, U61, U41, a__U23, a__U41, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, U14, s, U51, U15, tt, U16, a__U16, a__isNat, U52, a__U15, a__U32, a__U14, U11, a__U13, a__U31, U12, a__U12, U31, U13, a__U11, U32, a__U61, a__isNatKind

Strategy

There are no SCCs!

Problem 4: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

a__isNat#(plus(V1, V2)) → a__U11#(a__isNatKind(V1), V1, V2)a__U11#(tt, V1, V2) → a__U12#(a__isNatKind(V1), V1, V2)
a__isNat#(s(V1)) → a__U21#(a__isNatKind(V1), V1)a__U22#(tt, V1) → a__isNat#(V1)
a__U14#(tt, V1, V2) → a__U15#(a__isNat(V1), V2)a__U13#(tt, V1, V2) → a__U14#(a__isNatKind(V2), V1, V2)
a__U21#(tt, V1) → a__U22#(a__isNatKind(V1), V1)a__U12#(tt, V1, V2) → a__U13#(a__isNatKind(V2), V1, V2)
a__U15#(tt, V2) → a__isNat#(V2)a__U14#(tt, V1, V2) → a__isNat#(V1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, isNat, U64, U63, U62, U61, U41, a__U41, a__U23, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, s, U51, U14, tt, U15, a__isNat, a__U16, U16, a__U15, U52, a__U14, a__U32, a__U31, a__U13, U11, a__U12, U12, a__U11, U13, U31, a__U61, U32, a__isNatKind

Strategy

Polynomial Interpretation

Standard Usable rules

a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U16(X) → U16(X)
a__U32(tt) → tta__isNatKind(0) → tt
a__U12(X1, X2, X3) → U12(X1, X2, X3)a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)
a__isNat(0) → tta__isNat(X) → isNat(X)
a__U13(X1, X2, X3) → U13(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)a__U23(X) → U23(X)
a__U31(tt, V2) → a__U32(a__isNatKind(V2))a__U21(X1, X2) → U21(X1, X2)
a__U41(tt) → tta__U22(X1, X2) → U22(X1, X2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__U23(tt) → tta__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(X1, X2, X3) → U14(X1, X2, X3)
a__U41(X) → U41(X)a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)
a__U16(tt) → tta__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)
a__U22(tt, V1) → a__U23(a__isNat(V1))a__U31(X1, X2) → U31(X1, X2)
a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U32(X) → U32(X)
a__isNatKind(X) → isNatKind(X)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)

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

a__U11#(tt, V1, V2) → a__U12#(a__isNatKind(V1), V1, V2)a__U14#(tt, V1, V2) → a__U15#(a__isNat(V1), V2)
a__U14#(tt, V1, V2) → a__isNat#(V1)

Problem 7: DependencyGraph

Dependency Pair Problem

Dependency Pairs

a__isNat#(plus(V1, V2)) → a__U11#(a__isNatKind(V1), V1, V2)a__isNat#(s(V1)) → a__U21#(a__isNatKind(V1), V1)
a__U22#(tt, V1) → a__isNat#(V1)a__U13#(tt, V1, V2) → a__U14#(a__isNatKind(V2), V1, V2)
a__U15#(tt, V2) → a__isNat#(V2)a__U12#(tt, V1, V2) → a__U13#(a__isNatKind(V2), V1, V2)
a__U21#(tt, V1) → a__U22#(a__isNatKind(V1), V1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, U64, isNat, U63, U62, U61, U41, a__U23, a__U41, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, U14, s, U51, U15, tt, U16, a__U16, a__isNat, U52, a__U15, a__U32, a__U14, U11, a__U13, a__U31, U12, a__U12, U31, U13, a__U11, U32, a__U61, a__isNatKind

Strategy

The following SCCs where found

a__isNat#(s(V1)) → a__U21#(a__isNatKind(V1), V1)a__U22#(tt, V1) → a__isNat#(V1)
a__U21#(tt, V1) → a__U22#(a__isNatKind(V1), V1)

Problem 9: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

a__isNat#(s(V1)) → a__U21#(a__isNatKind(V1), V1)a__U22#(tt, V1) → a__isNat#(V1)
a__U21#(tt, V1) → a__U22#(a__isNatKind(V1), V1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, U64, isNat, U63, U62, U61, U41, a__U23, a__U41, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, U14, s, U51, U15, tt, U16, a__U16, a__isNat, U52, a__U15, a__U32, a__U14, U11, a__U13, a__U31, U12, a__U12, U31, U13, a__U11, U32, a__U61, a__isNatKind

Strategy

Polynomial Interpretation

Standard Usable rules

a__U41(X) → U41(X)a__U32(tt) → tt
a__isNatKind(0) → tta__U41(tt) → tt
a__U31(X1, X2) → U31(X1, X2)a__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__U32(X) → U32(X)
a__isNatKind(X) → isNatKind(X)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))

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

a__U22#(tt, V1) → a__isNat#(V1)

Problem 11: DependencyGraph

Dependency Pair Problem

Dependency Pairs

a__isNat#(s(V1)) → a__U21#(a__isNatKind(V1), V1)a__U21#(tt, V1) → a__U22#(a__isNatKind(V1), V1)

Rewrite Rules

a__U11(tt, V1, V2) → a__U12(a__isNatKind(V1), V1, V2)a__U12(tt, V1, V2) → a__U13(a__isNatKind(V2), V1, V2)
a__U13(tt, V1, V2) → a__U14(a__isNatKind(V2), V1, V2)a__U14(tt, V1, V2) → a__U15(a__isNat(V1), V2)
a__U15(tt, V2) → a__U16(a__isNat(V2))a__U16(tt) → tt
a__U21(tt, V1) → a__U22(a__isNatKind(V1), V1)a__U22(tt, V1) → a__U23(a__isNat(V1))
a__U23(tt) → tta__U31(tt, V2) → a__U32(a__isNatKind(V2))
a__U32(tt) → tta__U41(tt) → tt
a__U51(tt, N) → a__U52(a__isNatKind(N), N)a__U52(tt, N) → mark(N)
a__U61(tt, M, N) → a__U62(a__isNatKind(M), M, N)a__U62(tt, M, N) → a__U63(a__isNat(N), M, N)
a__U63(tt, M, N) → a__U64(a__isNatKind(N), M, N)a__U64(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__isNat(0) → tta__isNat(plus(V1, V2)) → a__U11(a__isNatKind(V1), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__U31(a__isNatKind(V1), V2)a__isNatKind(s(V1)) → a__U41(a__isNatKind(V1))
a__plus(N, 0) → a__U51(a__isNat(N), N)a__plus(N, s(M)) → a__U61(a__isNat(M), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(isNatKind(X)) → a__isNatKind(X)mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)mark(U15(X1, X2)) → a__U15(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)mark(U16(X)) → a__U16(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)mark(U22(X1, X2)) → a__U22(mark(X1), X2)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(U41(X)) → a__U41(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)mark(U62(X1, X2, X3)) → a__U62(mark(X1), X2, X3)
mark(U63(X1, X2, X3)) → a__U63(mark(X1), X2, X3)mark(U64(X1, X2, X3)) → a__U64(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))mark(tt) → tt
mark(s(X)) → s(mark(X))mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__isNatKind(X) → isNatKind(X)a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U14(X1, X2, X3) → U14(X1, X2, X3)a__U15(X1, X2) → U15(X1, X2)
a__isNat(X) → isNat(X)a__U16(X) → U16(X)
a__U21(X1, X2) → U21(X1, X2)a__U22(X1, X2) → U22(X1, X2)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__U41(X) → U41(X)
a__U51(X1, X2) → U51(X1, X2)a__U52(X1, X2) → U52(X1, X2)
a__U61(X1, X2, X3) → U61(X1, X2, X3)a__U62(X1, X2, X3) → U62(X1, X2, X3)
a__U63(X1, X2, X3) → U63(X1, X2, X3)a__U64(X1, X2, X3) → U64(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__U51, a__U52, isNat, U64, U63, U62, U61, U41, a__U41, a__U23, a__U22, U23, U21, a__U21, U22, a__U64, plus, a__U62, a__U63, isNatKind, a__plus, mark, 0, U51, U14, s, tt, U15, a__isNat, a__U16, U16, a__U15, U52, a__U14, a__U32, a__U31, a__U13, U11, a__U12, U12, a__U11, U13, U31, a__U61, U32, a__isNatKind

Strategy

There are no SCCs!