YES
The TRS could be proven terminating. The proof took 1633 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (505ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (123ms).
| | – Problem 5 was processed with processor DependencyGraph (1ms).
| | | – Problem 8 was processed with processor PolynomialLinearRange4 (23ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (407ms).
| | – Problem 6 was processed with processor DependencyGraph (2ms).
| – Problem 4 was processed with processor PolynomialLinearRange4 (193ms).
| | – Problem 7 was processed with processor DependencyGraph (12ms).
| | | – Problem 9 was processed with processor PolynomialLinearRange4 (104ms).
| | | | – Problem 10 was processed with processor DependencyGraph (3ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U15#(tt, V2) | → | U16#(isNat(V2)) | | U62#(tt, M, N) | → | isNat#(N) |
| plus#(N, 0) | → | isNat#(N) | | U12#(tt, V1, V2) | → | U13#(isNatKind(V2), V1, V2) |
| U13#(tt, V1, V2) | → | isNatKind#(V2) | | isNat#(s(V1)) | → | isNatKind#(V1) |
| isNat#(s(V1)) | → | U21#(isNatKind(V1), V1) | | U22#(tt, V1) | → | isNat#(V1) |
| isNatKind#(plus(V1, V2)) | → | U31#(isNatKind(V1), V2) | | U12#(tt, V1, V2) | → | isNatKind#(V2) |
| U64#(tt, M, N) | → | T(N) | | U61#(tt, M, N) | → | isNatKind#(M) |
| U21#(tt, V1) | → | U22#(isNatKind(V1), V1) | | U13#(tt, V1, V2) | → | U14#(isNatKind(V2), V1, V2) |
| plus#(N, s(M)) | → | isNat#(M) | | isNatKind#(s(V1)) | → | isNatKind#(V1) |
| U14#(tt, V1, V2) | → | U15#(isNat(V1), V2) | | U63#(tt, M, N) | → | isNatKind#(N) |
| isNat#(plus(V1, V2)) | → | U11#(isNatKind(V1), V1, V2) | | U15#(tt, V2) | → | isNat#(V2) |
| U31#(tt, V2) | → | isNatKind#(V2) | | U11#(tt, V1, V2) | → | U12#(isNatKind(V1), V1, V2) |
| U62#(tt, M, N) | → | U63#(isNat(N), M, N) | | U14#(tt, V1, V2) | → | isNat#(V1) |
| U11#(tt, V1, V2) | → | isNatKind#(V1) | | U22#(tt, V1) | → | U23#(isNat(V1)) |
| isNatKind#(plus(V1, V2)) | → | isNatKind#(V1) | | U61#(tt, M, N) | → | U62#(isNatKind(M), M, N) |
| U64#(tt, M, N) | → | plus#(N, M) | | plus#(N, 0) | → | U51#(isNat(N), N) |
| U51#(tt, N) | → | isNatKind#(N) | | U21#(tt, V1) | → | isNatKind#(V1) |
| U64#(tt, M, N) | → | T(M) | | plus#(N, s(M)) | → | U61#(isNat(M), M, N) |
| isNat#(plus(V1, V2)) | → | isNatKind#(V1) | | U52#(tt, N) | → | T(N) |
| U31#(tt, V2) | → | U32#(isNatKind(V2)) | | isNatKind#(s(V1)) | → | U41#(isNatKind(V1)) |
| U63#(tt, M, N) | → | U64#(isNatKind(N), M, N) | | U51#(tt, N) | → | U52#(isNatKind(N), N) |
Rewrite Rules
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) |
| U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) | | U14(tt, V1, V2) | → | U15(isNat(V1), V2) |
| U15(tt, V2) | → | U16(isNat(V2)) | | U16(tt) | → | tt |
| U21(tt, V1) | → | U22(isNatKind(V1), V1) | | U22(tt, V1) | → | U23(isNat(V1)) |
| U23(tt) | → | tt | | U31(tt, V2) | → | U32(isNatKind(V2)) |
| U32(tt) | → | tt | | U41(tt) | → | tt |
| U51(tt, N) | → | U52(isNatKind(N), N) | | U52(tt, N) | → | N |
| U61(tt, M, N) | → | U62(isNatKind(M), M, N) | | U62(tt, M, N) | → | U63(isNat(N), M, N) |
| U63(tt, M, N) | → | U64(isNatKind(N), M, N) | | U64(tt, M, N) | → | s(plus(N, M)) |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNatKind(0) | → | tt |
| isNatKind(plus(V1, V2)) | → | U31(isNatKind(V1), V2) | | isNatKind(s(V1)) | → | U41(isNatKind(V1)) |
| plus(N, 0) | → | U51(isNat(N), N) | | plus(N, s(M)) | → | U61(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, isNatKind, U64, isNat, U63, U62, 0, U61, s, U51, U14, U15, U41, tt, U16, U52, U11, U12, U31, U13, U23, U32, U21, U22
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(isNatKind) = μ(0) = μ(isNatKind#) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U64#) = μ(U31#) = μ(U13#) = μ(U21#) = μ(U23#) = μ(U62#) = μ(U52#) = μ(U64) = μ(U63) = μ(U41#) = μ(U62) = μ(U61) = μ(U41) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U14#) = μ(U12#) = μ(U22#) = μ(U63#) = μ(U61#) = μ(U51#) = μ(U51) = μ(U14) = μ(s) = μ(U15) = μ(U16) = μ(U52) = μ(U32#) = μ(U15#) = μ(U11) = μ(U12) = μ(U13) = μ(U31) = μ(U32) = {1}
μ(plus) = μ(plus#) = {1, 2}
The following SCCs where found
| isNatKind#(s(V1)) → isNatKind#(V1) | isNatKind#(plus(V1, V2)) → isNatKind#(V1) |
| isNatKind#(plus(V1, V2)) → U31#(isNatKind(V1), V2) | U31#(tt, V2) → isNatKind#(V2) |
| U14#(tt, V1, V2) → U15#(isNat(V1), V2) | U12#(tt, V1, V2) → U13#(isNatKind(V2), V1, V2) |
| isNat#(s(V1)) → U21#(isNatKind(V1), V1) | U22#(tt, V1) → isNat#(V1) |
| U15#(tt, V2) → isNat#(V2) | isNat#(plus(V1, V2)) → U11#(isNatKind(V1), V1, V2) |
| U11#(tt, V1, V2) → U12#(isNatKind(V1), V1, V2) | U13#(tt, V1, V2) → U14#(isNatKind(V2), V1, V2) |
| U21#(tt, V1) → U22#(isNatKind(V1), V1) | U14#(tt, V1, V2) → isNat#(V1) |
| plus#(N, s(M)) → U61#(isNat(M), M, N) | U61#(tt, M, N) → U62#(isNatKind(M), M, N) |
| U64#(tt, M, N) → plus#(N, M) | U62#(tt, M, N) → U63#(isNat(N), M, N) |
| U63#(tt, M, N) → U64#(isNatKind(N), M, N) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNatKind#(s(V1)) | → | isNatKind#(V1) | | isNatKind#(plus(V1, V2)) | → | isNatKind#(V1) |
| isNatKind#(plus(V1, V2)) | → | U31#(isNatKind(V1), V2) | | U31#(tt, V2) | → | isNatKind#(V2) |
Rewrite Rules
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) |
| U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) | | U14(tt, V1, V2) | → | U15(isNat(V1), V2) |
| U15(tt, V2) | → | U16(isNat(V2)) | | U16(tt) | → | tt |
| U21(tt, V1) | → | U22(isNatKind(V1), V1) | | U22(tt, V1) | → | U23(isNat(V1)) |
| U23(tt) | → | tt | | U31(tt, V2) | → | U32(isNatKind(V2)) |
| U32(tt) | → | tt | | U41(tt) | → | tt |
| U51(tt, N) | → | U52(isNatKind(N), N) | | U52(tt, N) | → | N |
| U61(tt, M, N) | → | U62(isNatKind(M), M, N) | | U62(tt, M, N) | → | U63(isNat(N), M, N) |
| U63(tt, M, N) | → | U64(isNatKind(N), M, N) | | U64(tt, M, N) | → | s(plus(N, M)) |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNatKind(0) | → | tt |
| isNatKind(plus(V1, V2)) | → | U31(isNatKind(V1), V2) | | isNatKind(s(V1)) | → | U41(isNatKind(V1)) |
| plus(N, 0) | → | U51(isNat(N), N) | | plus(N, s(M)) | → | U61(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, isNatKind, U64, isNat, U63, U62, 0, U61, s, U51, U14, U15, U41, tt, U16, U52, U11, U12, U31, U13, U23, U32, U21, U22
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(isNatKind) = μ(0) = μ(tt) = μ(isNatKind#) = μ(isNat#) = ∅
μ(U11#) = μ(U13#) = μ(U31#) = μ(U64#) = μ(U21#) = μ(U23#) = μ(U62#) = μ(U52#) = μ(U64) = μ(U63) = μ(U41#) = μ(U62) = μ(U61) = μ(U41) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U14#) = μ(U12#) = μ(U22#) = μ(U63#) = μ(U61#) = μ(U51#) = μ(s) = μ(U14) = μ(U51) = μ(U15) = μ(U16) = μ(U52) = μ(U32#) = μ(U11) = μ(U15#) = μ(U12) = μ(U31) = μ(U13) = μ(U32) = {1}
μ(plus) = μ(plus#) = {1, 2}
Polynomial Interpretation
- 0: 3
- U11(x,y,z): 0
- U12(x,y,z): 0
- U13(x,y,z): 0
- U14(x,y,z): 0
- U15(x,y): 0
- U16(x): 0
- U21(x,y): 0
- U22(x,y): 0
- U23(x): 0
- U31(x,y): 0
- U31#(x,y): 3y
- U32(x): 0
- U41(x): 0
- U51(x,y): 0
- U52(x,y): 0
- U61(x,y,z): 0
- U62(x,y,z): 0
- U63(x,y,z): 0
- U64(x,y,z): 0
- isNat(x): 0
- isNatKind(x): 0
- isNatKind#(x): 2x
- plus(x,y): 2y + 2x + 1
- s(x): 3x
- tt: 0
Standard Usable rules
| isNatKind(plus(V1, V2)) | → | U31(isNatKind(V1), V2) | | U32(tt) | → | tt |
| isNatKind(0) | → | tt | | U31(tt, V2) | → | U32(isNatKind(V2)) |
| U41(tt) | → | tt | | isNatKind(s(V1)) | → | U41(isNatKind(V1)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isNatKind#(plus(V1, V2)) | → | isNatKind#(V1) | | isNatKind#(plus(V1, V2)) | → | U31#(isNatKind(V1), V2) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isNatKind#(s(V1)) | → | isNatKind#(V1) | | U31#(tt, V2) | → | isNatKind#(V2) |
Rewrite Rules
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) |
| U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) | | U14(tt, V1, V2) | → | U15(isNat(V1), V2) |
| U15(tt, V2) | → | U16(isNat(V2)) | | U16(tt) | → | tt |
| U21(tt, V1) | → | U22(isNatKind(V1), V1) | | U22(tt, V1) | → | U23(isNat(V1)) |
| U23(tt) | → | tt | | U31(tt, V2) | → | U32(isNatKind(V2)) |
| U32(tt) | → | tt | | U41(tt) | → | tt |
| U51(tt, N) | → | U52(isNatKind(N), N) | | U52(tt, N) | → | N |
| U61(tt, M, N) | → | U62(isNatKind(M), M, N) | | U62(tt, M, N) | → | U63(isNat(N), M, N) |
| U63(tt, M, N) | → | U64(isNatKind(N), M, N) | | U64(tt, M, N) | → | s(plus(N, M)) |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNatKind(0) | → | tt |
| isNatKind(plus(V1, V2)) | → | U31(isNatKind(V1), V2) | | isNatKind(s(V1)) | → | U41(isNatKind(V1)) |
| plus(N, 0) | → | U51(isNat(N), N) | | plus(N, s(M)) | → | U61(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, isNatKind, U64, isNat, U63, U62, 0, U61, s, U51, U14, tt, U15, U41, U16, U52, U11, U12, U13, U31, U32, U23, U21, U22
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(isNatKind) = μ(0) = μ(isNatKind#) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U64#) = μ(U31#) = μ(U13#) = μ(U21#) = μ(U23#) = μ(U62#) = μ(U52#) = μ(U64) = μ(U63) = μ(U41#) = μ(U62) = μ(U61) = μ(U41) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U14#) = μ(U12#) = μ(U22#) = μ(U63#) = μ(U61#) = μ(U51#) = μ(U51) = μ(U14) = μ(s) = μ(U15) = μ(U16) = μ(U52) = μ(U32#) = μ(U15#) = μ(U11) = μ(U12) = μ(U13) = μ(U31) = μ(U32) = {1}
μ(plus) = μ(plus#) = {1, 2}
The following SCCs where found
| isNatKind#(s(V1)) → isNatKind#(V1) |
Problem 8: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNatKind#(s(V1)) | → | isNatKind#(V1) |
Rewrite Rules
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) |
| U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) | | U14(tt, V1, V2) | → | U15(isNat(V1), V2) |
| U15(tt, V2) | → | U16(isNat(V2)) | | U16(tt) | → | tt |
| U21(tt, V1) | → | U22(isNatKind(V1), V1) | | U22(tt, V1) | → | U23(isNat(V1)) |
| U23(tt) | → | tt | | U31(tt, V2) | → | U32(isNatKind(V2)) |
| U32(tt) | → | tt | | U41(tt) | → | tt |
| U51(tt, N) | → | U52(isNatKind(N), N) | | U52(tt, N) | → | N |
| U61(tt, M, N) | → | U62(isNatKind(M), M, N) | | U62(tt, M, N) | → | U63(isNat(N), M, N) |
| U63(tt, M, N) | → | U64(isNatKind(N), M, N) | | U64(tt, M, N) | → | s(plus(N, M)) |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNatKind(0) | → | tt |
| isNatKind(plus(V1, V2)) | → | U31(isNatKind(V1), V2) | | isNatKind(s(V1)) | → | U41(isNatKind(V1)) |
| plus(N, 0) | → | U51(isNat(N), N) | | plus(N, s(M)) | → | U61(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, isNatKind, U64, isNat, U63, U62, 0, U61, s, U51, U14, tt, U15, U41, U16, U52, U11, U12, U13, U31, U32, U23, U21, U22
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(isNatKind) = μ(0) = μ(tt) = μ(isNatKind#) = μ(isNat#) = ∅
μ(U11#) = μ(U13#) = μ(U31#) = μ(U64#) = μ(U21#) = μ(U23#) = μ(U62#) = μ(U52#) = μ(U64) = μ(U63) = μ(U41#) = μ(U62) = μ(U61) = μ(U41) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U14#) = μ(U12#) = μ(U22#) = μ(U63#) = μ(U61#) = μ(U51#) = μ(s) = μ(U14) = μ(U51) = μ(U15) = μ(U16) = μ(U52) = μ(U32#) = μ(U11) = μ(U15#) = μ(U12) = μ(U31) = μ(U13) = μ(U32) = {1}
μ(plus) = μ(plus#) = {1, 2}
Polynomial Interpretation
- 0: 0
- U11(x,y,z): 0
- U12(x,y,z): 0
- U13(x,y,z): 0
- U14(x,y,z): 0
- U15(x,y): 0
- U16(x): 0
- U21(x,y): 0
- U22(x,y): 0
- U23(x): 0
- U31(x,y): 0
- U32(x): 0
- U41(x): 0
- U51(x,y): 0
- U52(x,y): 0
- U61(x,y,z): 0
- U62(x,y,z): 0
- U63(x,y,z): 0
- U64(x,y,z): 0
- isNat(x): 0
- isNatKind(x): 0
- isNatKind#(x): x + 1
- plus(x,y): 0
- s(x): x + 1
- tt: 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isNatKind#(s(V1)) | → | isNatKind#(V1) |
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| plus#(N, s(M)) | → | U61#(isNat(M), M, N) | | U61#(tt, M, N) | → | U62#(isNatKind(M), M, N) |
| U64#(tt, M, N) | → | plus#(N, M) | | U62#(tt, M, N) | → | U63#(isNat(N), M, N) |
| U63#(tt, M, N) | → | U64#(isNatKind(N), M, N) |
Rewrite Rules
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) |
| U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) | | U14(tt, V1, V2) | → | U15(isNat(V1), V2) |
| U15(tt, V2) | → | U16(isNat(V2)) | | U16(tt) | → | tt |
| U21(tt, V1) | → | U22(isNatKind(V1), V1) | | U22(tt, V1) | → | U23(isNat(V1)) |
| U23(tt) | → | tt | | U31(tt, V2) | → | U32(isNatKind(V2)) |
| U32(tt) | → | tt | | U41(tt) | → | tt |
| U51(tt, N) | → | U52(isNatKind(N), N) | | U52(tt, N) | → | N |
| U61(tt, M, N) | → | U62(isNatKind(M), M, N) | | U62(tt, M, N) | → | U63(isNat(N), M, N) |
| U63(tt, M, N) | → | U64(isNatKind(N), M, N) | | U64(tt, M, N) | → | s(plus(N, M)) |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNatKind(0) | → | tt |
| isNatKind(plus(V1, V2)) | → | U31(isNatKind(V1), V2) | | isNatKind(s(V1)) | → | U41(isNatKind(V1)) |
| plus(N, 0) | → | U51(isNat(N), N) | | plus(N, s(M)) | → | U61(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, isNatKind, U64, isNat, U63, U62, 0, U61, s, U51, U14, U15, U41, tt, U16, U52, U11, U12, U31, U13, U23, U32, U21, U22
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(isNatKind) = μ(0) = μ(tt) = μ(isNatKind#) = μ(isNat#) = ∅
μ(U11#) = μ(U13#) = μ(U31#) = μ(U64#) = μ(U21#) = μ(U23#) = μ(U62#) = μ(U52#) = μ(U64) = μ(U63) = μ(U41#) = μ(U62) = μ(U61) = μ(U41) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U14#) = μ(U12#) = μ(U22#) = μ(U63#) = μ(U61#) = μ(U51#) = μ(s) = μ(U14) = μ(U51) = μ(U15) = μ(U16) = μ(U52) = μ(U32#) = μ(U11) = μ(U15#) = μ(U12) = μ(U31) = μ(U13) = μ(U32) = {1}
μ(plus) = μ(plus#) = {1, 2}
Polynomial Interpretation
- 0: 2
- U11(x,y,z): x
- U12(x,y,z): x
- U13(x,y,z): 2
- U14(x,y,z): x
- U15(x,y): x
- U16(x): x
- U21(x,y): 2
- U22(x,y): x
- U23(x): x
- U31(x,y): x
- U32(x): x
- U41(x): 2
- U51(x,y): y + x
- U52(x,y): y + x
- U61(x,y,z): z + y + 2
- U61#(x,y,z): 2y + x
- U62(x,y,z): z + y + 2
- U62#(x,y,z): 2y + x
- U63(x,y,z): z + y + 2
- U63#(x,y,z): 2y + x
- U64(x,y,z): z + y + x
- U64#(x,y,z): 2y + x
- isNat(x): 2
- isNatKind(x): 2
- plus(x,y): y + x + 1
- plus#(x,y): 2y
- s(x): x + 1
- tt: 2
Standard Usable rules
| isNatKind(plus(V1, V2)) | → | U31(isNatKind(V1), V2) | | U15(tt, V2) | → | U16(isNat(V2)) |
| U64(tt, M, N) | → | s(plus(N, M)) | | isNat(s(V1)) | → | U21(isNatKind(V1), V1) |
| U41(tt) | → | tt | | U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) |
| U51(tt, N) | → | U52(isNatKind(N), N) | | U32(tt) | → | tt |
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | isNatKind(0) | → | tt |
| U31(tt, V2) | → | U32(isNatKind(V2)) | | U61(tt, M, N) | → | U62(isNatKind(M), M, N) |
| isNat(0) | → | tt | | U23(tt) | → | tt |
| U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) | | U14(tt, V1, V2) | → | U15(isNat(V1), V2) |
| U63(tt, M, N) | → | U64(isNatKind(N), M, N) | | isNatKind(s(V1)) | → | U41(isNatKind(V1)) |
| plus(N, s(M)) | → | U61(isNat(M), M, N) | | U16(tt) | → | tt |
| U52(tt, N) | → | N | | plus(N, 0) | → | U51(isNat(N), N) |
| U62(tt, M, N) | → | U63(isNat(N), M, N) | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| U22(tt, V1) | → | U23(isNat(V1)) | | U21(tt, V1) | → | U22(isNatKind(V1), V1) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U64#(tt, M, N) | → | plus#(N, M) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| plus#(N, s(M)) | → | U61#(isNat(M), M, N) | | U61#(tt, M, N) | → | U62#(isNatKind(M), M, N) |
| U62#(tt, M, N) | → | U63#(isNat(N), M, N) | | U63#(tt, M, N) | → | U64#(isNatKind(N), M, N) |
Rewrite Rules
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) |
| U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) | | U14(tt, V1, V2) | → | U15(isNat(V1), V2) |
| U15(tt, V2) | → | U16(isNat(V2)) | | U16(tt) | → | tt |
| U21(tt, V1) | → | U22(isNatKind(V1), V1) | | U22(tt, V1) | → | U23(isNat(V1)) |
| U23(tt) | → | tt | | U31(tt, V2) | → | U32(isNatKind(V2)) |
| U32(tt) | → | tt | | U41(tt) | → | tt |
| U51(tt, N) | → | U52(isNatKind(N), N) | | U52(tt, N) | → | N |
| U61(tt, M, N) | → | U62(isNatKind(M), M, N) | | U62(tt, M, N) | → | U63(isNat(N), M, N) |
| U63(tt, M, N) | → | U64(isNatKind(N), M, N) | | U64(tt, M, N) | → | s(plus(N, M)) |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNatKind(0) | → | tt |
| isNatKind(plus(V1, V2)) | → | U31(isNatKind(V1), V2) | | isNatKind(s(V1)) | → | U41(isNatKind(V1)) |
| plus(N, 0) | → | U51(isNat(N), N) | | plus(N, s(M)) | → | U61(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, isNatKind, U64, isNat, U63, U62, 0, U61, s, U51, U14, tt, U15, U41, U16, U52, U11, U12, U13, U31, U32, U23, U21, U22
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(isNatKind) = μ(0) = μ(isNatKind#) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U64#) = μ(U31#) = μ(U13#) = μ(U21#) = μ(U23#) = μ(U62#) = μ(U52#) = μ(U64) = μ(U63) = μ(U41#) = μ(U62) = μ(U61) = μ(U41) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U14#) = μ(U12#) = μ(U22#) = μ(U63#) = μ(U61#) = μ(U51#) = μ(U51) = μ(U14) = μ(s) = μ(U15) = μ(U16) = μ(U52) = μ(U32#) = μ(U15#) = μ(U11) = μ(U12) = μ(U13) = μ(U31) = μ(U32) = {1}
μ(plus) = μ(plus#) = {1, 2}
There are no SCCs!
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| U14#(tt, V1, V2) | → | U15#(isNat(V1), V2) | | U12#(tt, V1, V2) | → | U13#(isNatKind(V2), V1, V2) |
| isNat#(s(V1)) | → | U21#(isNatKind(V1), V1) | | U22#(tt, V1) | → | isNat#(V1) |
| U15#(tt, V2) | → | isNat#(V2) | | isNat#(plus(V1, V2)) | → | U11#(isNatKind(V1), V1, V2) |
| U11#(tt, V1, V2) | → | U12#(isNatKind(V1), V1, V2) | | U13#(tt, V1, V2) | → | U14#(isNatKind(V2), V1, V2) |
| U21#(tt, V1) | → | U22#(isNatKind(V1), V1) | | U14#(tt, V1, V2) | → | isNat#(V1) |
Rewrite Rules
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) |
| U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) | | U14(tt, V1, V2) | → | U15(isNat(V1), V2) |
| U15(tt, V2) | → | U16(isNat(V2)) | | U16(tt) | → | tt |
| U21(tt, V1) | → | U22(isNatKind(V1), V1) | | U22(tt, V1) | → | U23(isNat(V1)) |
| U23(tt) | → | tt | | U31(tt, V2) | → | U32(isNatKind(V2)) |
| U32(tt) | → | tt | | U41(tt) | → | tt |
| U51(tt, N) | → | U52(isNatKind(N), N) | | U52(tt, N) | → | N |
| U61(tt, M, N) | → | U62(isNatKind(M), M, N) | | U62(tt, M, N) | → | U63(isNat(N), M, N) |
| U63(tt, M, N) | → | U64(isNatKind(N), M, N) | | U64(tt, M, N) | → | s(plus(N, M)) |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNatKind(0) | → | tt |
| isNatKind(plus(V1, V2)) | → | U31(isNatKind(V1), V2) | | isNatKind(s(V1)) | → | U41(isNatKind(V1)) |
| plus(N, 0) | → | U51(isNat(N), N) | | plus(N, s(M)) | → | U61(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, isNatKind, U64, isNat, U63, U62, 0, U61, s, U51, U14, U15, U41, tt, U16, U52, U11, U12, U31, U13, U23, U32, U21, U22
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(isNatKind) = μ(0) = μ(tt) = μ(isNatKind#) = μ(isNat#) = ∅
μ(U11#) = μ(U13#) = μ(U31#) = μ(U64#) = μ(U21#) = μ(U23#) = μ(U62#) = μ(U52#) = μ(U64) = μ(U63) = μ(U41#) = μ(U62) = μ(U61) = μ(U41) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U14#) = μ(U12#) = μ(U22#) = μ(U63#) = μ(U61#) = μ(U51#) = μ(s) = μ(U14) = μ(U51) = μ(U15) = μ(U16) = μ(U52) = μ(U32#) = μ(U11) = μ(U15#) = μ(U12) = μ(U31) = μ(U13) = μ(U32) = {1}
μ(plus) = μ(plus#) = {1, 2}
Polynomial Interpretation
- 0: 0
- U11(x,y,z): 0
- U11#(x,y,z): 3z + 3y + x + 1
- U12(x,y,z): 0
- U12#(x,y,z): 3z + 2y + x
- U13(x,y,z): 0
- U13#(x,y,z): 3z + 2y
- U14(x,y,z): 0
- U14#(x,y,z): 2z + 2y
- U15(x,y): 0
- U15#(x,y): 2y
- U16(x): 0
- U21(x,y): 0
- U21#(x,y): 2y + 2
- U22(x,y): 0
- U22#(x,y): 2y
- U23(x): 0
- U31(x,y): 2y + x + 1
- U32(x): 1
- U41(x): 1
- U51(x,y): 0
- U52(x,y): 0
- U61(x,y,z): 0
- U62(x,y,z): 0
- U63(x,y,z): 0
- U64(x,y,z): 0
- isNat(x): 0
- isNat#(x): 2x
- isNatKind(x): x + 1
- plus(x,y): 2y + 2x + 1
- s(x): x + 1
- tt: 0
Standard Usable rules
| isNat(0) | → | tt | | isNatKind(plus(V1, V2)) | → | U31(isNatKind(V1), V2) |
| U23(tt) | → | tt | | U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) |
| U14(tt, V1, V2) | → | U15(isNat(V1), V2) | | U15(tt, V2) | → | U16(isNat(V2)) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | U41(tt) | → | tt |
| U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) | | isNatKind(s(V1)) | → | U41(isNatKind(V1)) |
| U16(tt) | → | tt | | U32(tt) | → | tt |
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| U22(tt, V1) | → | U23(isNat(V1)) | | U21(tt, V1) | → | U22(isNatKind(V1), V1) |
| isNatKind(0) | → | tt | | U31(tt, V2) | → | U32(isNatKind(V2)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U21#(tt, V1) | → | U22#(isNatKind(V1), V1) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U14#(tt, V1, V2) | → | U15#(isNat(V1), V2) | | U12#(tt, V1, V2) | → | U13#(isNatKind(V2), V1, V2) |
| isNat#(s(V1)) | → | U21#(isNatKind(V1), V1) | | U22#(tt, V1) | → | isNat#(V1) |
| isNat#(plus(V1, V2)) | → | U11#(isNatKind(V1), V1, V2) | | U15#(tt, V2) | → | isNat#(V2) |
| U11#(tt, V1, V2) | → | U12#(isNatKind(V1), V1, V2) | | U13#(tt, V1, V2) | → | U14#(isNatKind(V2), V1, V2) |
| U14#(tt, V1, V2) | → | isNat#(V1) |
Rewrite Rules
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) |
| U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) | | U14(tt, V1, V2) | → | U15(isNat(V1), V2) |
| U15(tt, V2) | → | U16(isNat(V2)) | | U16(tt) | → | tt |
| U21(tt, V1) | → | U22(isNatKind(V1), V1) | | U22(tt, V1) | → | U23(isNat(V1)) |
| U23(tt) | → | tt | | U31(tt, V2) | → | U32(isNatKind(V2)) |
| U32(tt) | → | tt | | U41(tt) | → | tt |
| U51(tt, N) | → | U52(isNatKind(N), N) | | U52(tt, N) | → | N |
| U61(tt, M, N) | → | U62(isNatKind(M), M, N) | | U62(tt, M, N) | → | U63(isNat(N), M, N) |
| U63(tt, M, N) | → | U64(isNatKind(N), M, N) | | U64(tt, M, N) | → | s(plus(N, M)) |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNatKind(0) | → | tt |
| isNatKind(plus(V1, V2)) | → | U31(isNatKind(V1), V2) | | isNatKind(s(V1)) | → | U41(isNatKind(V1)) |
| plus(N, 0) | → | U51(isNat(N), N) | | plus(N, s(M)) | → | U61(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, isNatKind, U64, isNat, U63, U62, 0, U61, s, U51, U14, tt, U15, U41, U16, U52, U11, U12, U13, U31, U32, U23, U21, U22
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(isNatKind) = μ(0) = μ(isNatKind#) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U64#) = μ(U31#) = μ(U13#) = μ(U21#) = μ(U23#) = μ(U62#) = μ(U52#) = μ(U64) = μ(U63) = μ(U41#) = μ(U62) = μ(U61) = μ(U41) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U14#) = μ(U12#) = μ(U22#) = μ(U63#) = μ(U61#) = μ(U51#) = μ(U51) = μ(U14) = μ(s) = μ(U15) = μ(U16) = μ(U52) = μ(U32#) = μ(U15#) = μ(U11) = μ(U12) = μ(U13) = μ(U31) = μ(U32) = {1}
μ(plus) = μ(plus#) = {1, 2}
The following SCCs where found
| U14#(tt, V1, V2) → U15#(isNat(V1), V2) | U12#(tt, V1, V2) → U13#(isNatKind(V2), V1, V2) |
| U15#(tt, V2) → isNat#(V2) | isNat#(plus(V1, V2)) → U11#(isNatKind(V1), V1, V2) |
| U11#(tt, V1, V2) → U12#(isNatKind(V1), V1, V2) | U13#(tt, V1, V2) → U14#(isNatKind(V2), V1, V2) |
| U14#(tt, V1, V2) → isNat#(V1) |
Problem 9: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| U14#(tt, V1, V2) | → | U15#(isNat(V1), V2) | | U12#(tt, V1, V2) | → | U13#(isNatKind(V2), V1, V2) |
| U15#(tt, V2) | → | isNat#(V2) | | isNat#(plus(V1, V2)) | → | U11#(isNatKind(V1), V1, V2) |
| U11#(tt, V1, V2) | → | U12#(isNatKind(V1), V1, V2) | | U13#(tt, V1, V2) | → | U14#(isNatKind(V2), V1, V2) |
| U14#(tt, V1, V2) | → | isNat#(V1) |
Rewrite Rules
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) |
| U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) | | U14(tt, V1, V2) | → | U15(isNat(V1), V2) |
| U15(tt, V2) | → | U16(isNat(V2)) | | U16(tt) | → | tt |
| U21(tt, V1) | → | U22(isNatKind(V1), V1) | | U22(tt, V1) | → | U23(isNat(V1)) |
| U23(tt) | → | tt | | U31(tt, V2) | → | U32(isNatKind(V2)) |
| U32(tt) | → | tt | | U41(tt) | → | tt |
| U51(tt, N) | → | U52(isNatKind(N), N) | | U52(tt, N) | → | N |
| U61(tt, M, N) | → | U62(isNatKind(M), M, N) | | U62(tt, M, N) | → | U63(isNat(N), M, N) |
| U63(tt, M, N) | → | U64(isNatKind(N), M, N) | | U64(tt, M, N) | → | s(plus(N, M)) |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNatKind(0) | → | tt |
| isNatKind(plus(V1, V2)) | → | U31(isNatKind(V1), V2) | | isNatKind(s(V1)) | → | U41(isNatKind(V1)) |
| plus(N, 0) | → | U51(isNat(N), N) | | plus(N, s(M)) | → | U61(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, isNatKind, U64, isNat, U63, U62, 0, U61, s, U51, U14, tt, U15, U41, U16, U52, U11, U12, U13, U31, U32, U23, U21, U22
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(isNatKind) = μ(0) = μ(tt) = μ(isNatKind#) = μ(isNat#) = ∅
μ(U11#) = μ(U13#) = μ(U31#) = μ(U64#) = μ(U21#) = μ(U23#) = μ(U62#) = μ(U52#) = μ(U64) = μ(U63) = μ(U41#) = μ(U62) = μ(U61) = μ(U41) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U14#) = μ(U12#) = μ(U22#) = μ(U63#) = μ(U61#) = μ(U51#) = μ(s) = μ(U14) = μ(U51) = μ(U15) = μ(U16) = μ(U52) = μ(U32#) = μ(U11) = μ(U15#) = μ(U12) = μ(U31) = μ(U13) = μ(U32) = {1}
μ(plus) = μ(plus#) = {1, 2}
Polynomial Interpretation
- 0: 0
- U11(x,y,z): 2z + 2y + 2
- U11#(x,y,z): 3z + 3y + 2
- U12(x,y,z): z + y + 1
- U12#(x,y,z): 2z + 2y + 2
- U13(x,y,z): z + 1
- U13#(x,y,z): 2z + 2y
- U14(x,y,z): z + 1
- U14#(x,y,z): 2z + 2y
- U15(x,y): 1
- U15#(x,y): 2y
- U16(x): 0
- U21(x,y): 0
- U22(x,y): 0
- U23(x): 0
- U31(x,y): 0
- U32(x): 0
- U41(x): x
- U51(x,y): 0
- U52(x,y): 0
- U61(x,y,z): 0
- U62(x,y,z): 0
- U63(x,y,z): 0
- U64(x,y,z): 0
- isNat(x): 2x
- isNat#(x): 2x
- isNatKind(x): 2
- plus(x,y): 2y + 3x + 1
- s(x): 0
- tt: 0
Standard Usable rules
| isNat(0) | → | tt | | isNatKind(plus(V1, V2)) | → | U31(isNatKind(V1), V2) |
| U23(tt) | → | tt | | U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) |
| U14(tt, V1, V2) | → | U15(isNat(V1), V2) | | U15(tt, V2) | → | U16(isNat(V2)) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | U41(tt) | → | tt |
| U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) | | isNatKind(s(V1)) | → | U41(isNatKind(V1)) |
| U16(tt) | → | tt | | U32(tt) | → | tt |
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| U22(tt, V1) | → | U23(isNat(V1)) | | U21(tt, V1) | → | U22(isNatKind(V1), V1) |
| isNatKind(0) | → | tt | | U31(tt, V2) | → | U32(isNatKind(V2)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U12#(tt, V1, V2) | → | U13#(isNatKind(V2), V1, V2) |
Problem 10: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U14#(tt, V1, V2) | → | U15#(isNat(V1), V2) | | isNat#(plus(V1, V2)) | → | U11#(isNatKind(V1), V1, V2) |
| U15#(tt, V2) | → | isNat#(V2) | | U11#(tt, V1, V2) | → | U12#(isNatKind(V1), V1, V2) |
| U13#(tt, V1, V2) | → | U14#(isNatKind(V2), V1, V2) | | U14#(tt, V1, V2) | → | isNat#(V1) |
Rewrite Rules
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) |
| U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) | | U14(tt, V1, V2) | → | U15(isNat(V1), V2) |
| U15(tt, V2) | → | U16(isNat(V2)) | | U16(tt) | → | tt |
| U21(tt, V1) | → | U22(isNatKind(V1), V1) | | U22(tt, V1) | → | U23(isNat(V1)) |
| U23(tt) | → | tt | | U31(tt, V2) | → | U32(isNatKind(V2)) |
| U32(tt) | → | tt | | U41(tt) | → | tt |
| U51(tt, N) | → | U52(isNatKind(N), N) | | U52(tt, N) | → | N |
| U61(tt, M, N) | → | U62(isNatKind(M), M, N) | | U62(tt, M, N) | → | U63(isNat(N), M, N) |
| U63(tt, M, N) | → | U64(isNatKind(N), M, N) | | U64(tt, M, N) | → | s(plus(N, M)) |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNatKind(0) | → | tt |
| isNatKind(plus(V1, V2)) | → | U31(isNatKind(V1), V2) | | isNatKind(s(V1)) | → | U41(isNatKind(V1)) |
| plus(N, 0) | → | U51(isNat(N), N) | | plus(N, s(M)) | → | U61(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, isNatKind, U64, isNat, U63, U62, 0, U61, s, U51, U14, U41, tt, U15, U16, U52, U11, U12, U31, U13, U23, U32, U21, U22
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(isNatKind) = μ(0) = μ(isNatKind#) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U64#) = μ(U31#) = μ(U13#) = μ(U21#) = μ(U23#) = μ(U62#) = μ(U52#) = μ(U64) = μ(U63) = μ(U41#) = μ(U62) = μ(U61) = μ(U41) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U14#) = μ(U12#) = μ(U22#) = μ(U63#) = μ(U61#) = μ(U51#) = μ(U51) = μ(U14) = μ(s) = μ(U15) = μ(U16) = μ(U52) = μ(U32#) = μ(U15#) = μ(U11) = μ(U12) = μ(U13) = μ(U31) = μ(U32) = {1}
μ(plus) = μ(plus#) = {1, 2}
There are no SCCs!