TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60591 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (1135ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (4ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (3ms), PolynomialOrderingProcessor (0ms), DependencyGraph (4ms), PolynomialLinearRange4 (538ms), DependencyGraph (4ms), PolynomialLinearRange4 (441ms), DependencyGraph (4ms), PolynomialLinearRange4 (374ms), DependencyGraph (2ms), PolynomialLinearRange4 (412ms), DependencyGraph (3ms), ReductionPairSAT (1117ms), DependencyGraph (2ms), SizeChangePrinciple (timeout)].
| – Problem 3 was processed with processor PolynomialLinearRange4 (276ms).
| | – Problem 6 was processed with processor DependencyGraph (36ms).
| | | – Problem 8 was processed with processor PolynomialLinearRange4 (193ms).
| | | | – Problem 10 was processed with processor DependencyGraph (9ms).
| | | | | – Problem 11 was processed with processor PolynomialLinearRange4 (89ms).
| | | | | | – Problem 12 was processed with processor DependencyGraph (3ms).
| – Problem 4 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (16ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (3ms), PolynomialOrderingProcessor (0ms), DependencyGraph (3ms), PolynomialLinearRange4 (400ms), DependencyGraph (4ms), PolynomialLinearRange4 (378ms), DependencyGraph (4ms), PolynomialLinearRange4 (296ms), DependencyGraph (2ms), PolynomialLinearRange4 (287ms), DependencyGraph (2ms), ReductionPairSAT (1032ms), DependencyGraph (2ms)].
| – Problem 5 was processed with processor PolynomialLinearRange4 (54ms).
| | – Problem 7 was processed with processor DependencyGraph (5ms).
| | | – Problem 9 was processed with processor PolynomialLinearRange4 (48ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| U82#(tt, M, N) | → | U83#(isNat(N), M, N) | | U83#(tt, M, N) | → | U84#(isNatKind(N), M, N) |
| plus#(N, s(M)) | → | U81#(isNat(M), M, N) | | U84#(tt, M, N) | → | plus#(N, M) |
| U81#(tt, M, N) | → | U82#(isNatKind(M), M, N) |
Rewrite Rules
| U101(tt, M, N) | → | U102(isNatKind(M), M, N) | | U102(tt, M, N) | → | U103(isNat(N), M, N) |
| U103(tt, M, N) | → | U104(isNatKind(N), M, N) | | U104(tt, M, N) | → | plus(x(N, M), N) |
| 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, V1, V2) | → | U32(isNatKind(V1), V1, V2) |
| U32(tt, V1, V2) | → | U33(isNatKind(V2), V1, V2) | | U33(tt, V1, V2) | → | U34(isNatKind(V2), V1, V2) |
| U34(tt, V1, V2) | → | U35(isNat(V1), V2) | | U35(tt, V2) | → | U36(isNat(V2)) |
| U36(tt) | → | tt | | U41(tt, V2) | → | U42(isNatKind(V2)) |
| U42(tt) | → | tt | | U51(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | U62(tt) | → | tt |
| U71(tt, N) | → | U72(isNatKind(N), N) | | U72(tt, N) | → | N |
| U81(tt, M, N) | → | U82(isNatKind(M), M, N) | | U82(tt, M, N) | → | U83(isNat(N), M, N) |
| U83(tt, M, N) | → | U84(isNatKind(N), M, N) | | U84(tt, M, N) | → | s(plus(N, M)) |
| U91(tt, N) | → | U92(isNatKind(N)) | | U92(tt) | → | 0 |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNat(x(V1, V2)) | → | U31(isNatKind(V1), V1, V2) |
| isNatKind(0) | → | tt | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| isNatKind(s(V1)) | → | U51(isNatKind(V1)) | | isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
| plus(N, 0) | → | U71(isNat(N), N) | | plus(N, s(M)) | → | U81(isNat(M), M, N) |
| x(N, 0) | → | U91(isNat(N), N) | | x(N, s(M)) | → | U101(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: U104, isNat, U62, U61, U42, U92, U41, U91, U23, U21, U22, plus, isNatKind, U83, U84, U71, U36, U72, 0, s, U51, U14, tt, U15, U82, U16, U81, U11, U12, U13, U31, U102, U32, U103, U33, U34, x, U101, U35
Open Dependency Pair Problem 4
Dependency Pairs
| x#(N, s(M)) | → | U101#(isNat(M), M, N) | | U102#(tt, M, N) | → | U103#(isNat(N), M, N) |
| U104#(tt, M, N) | → | x#(N, M) | | U103#(tt, M, N) | → | U104#(isNatKind(N), M, N) |
| U101#(tt, M, N) | → | U102#(isNatKind(M), M, N) |
Rewrite Rules
| U101(tt, M, N) | → | U102(isNatKind(M), M, N) | | U102(tt, M, N) | → | U103(isNat(N), M, N) |
| U103(tt, M, N) | → | U104(isNatKind(N), M, N) | | U104(tt, M, N) | → | plus(x(N, M), N) |
| 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, V1, V2) | → | U32(isNatKind(V1), V1, V2) |
| U32(tt, V1, V2) | → | U33(isNatKind(V2), V1, V2) | | U33(tt, V1, V2) | → | U34(isNatKind(V2), V1, V2) |
| U34(tt, V1, V2) | → | U35(isNat(V1), V2) | | U35(tt, V2) | → | U36(isNat(V2)) |
| U36(tt) | → | tt | | U41(tt, V2) | → | U42(isNatKind(V2)) |
| U42(tt) | → | tt | | U51(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | U62(tt) | → | tt |
| U71(tt, N) | → | U72(isNatKind(N), N) | | U72(tt, N) | → | N |
| U81(tt, M, N) | → | U82(isNatKind(M), M, N) | | U82(tt, M, N) | → | U83(isNat(N), M, N) |
| U83(tt, M, N) | → | U84(isNatKind(N), M, N) | | U84(tt, M, N) | → | s(plus(N, M)) |
| U91(tt, N) | → | U92(isNatKind(N)) | | U92(tt) | → | 0 |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNat(x(V1, V2)) | → | U31(isNatKind(V1), V1, V2) |
| isNatKind(0) | → | tt | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| isNatKind(s(V1)) | → | U51(isNatKind(V1)) | | isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
| plus(N, 0) | → | U71(isNat(N), N) | | plus(N, s(M)) | → | U81(isNat(M), M, N) |
| x(N, 0) | → | U91(isNat(N), N) | | x(N, s(M)) | → | U101(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: U104, isNat, U62, U61, U42, U92, U41, U91, U23, U21, U22, plus, isNatKind, U83, U84, U71, U36, U72, 0, s, U51, U14, tt, U15, U82, U16, U81, U11, U12, U13, U31, U102, U32, U103, U33, U34, x, U101, U35
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U15#(tt, V2) | → | U16#(isNat(V2)) | | U83#(tt, M, N) | → | isNatKind#(N) |
| x#(N, s(M)) | → | U101#(isNat(M), M, N) | | plus#(N, 0) | → | U71#(isNat(N), N) |
| isNatKind#(plus(V1, V2)) | → | U41#(isNatKind(V1), V2) | | isNat#(s(V1)) | → | isNatKind#(V1) |
| U13#(tt, V1, V2) | → | isNatKind#(V2) | | isNat#(s(V1)) | → | U21#(isNatKind(V1), V1) |
| U12#(tt, V1, V2) | → | isNatKind#(V2) | | U104#(tt, M, N) | → | x#(N, M) |
| U41#(tt, V2) | → | U42#(isNatKind(V2)) | | U13#(tt, V1, V2) | → | U14#(isNatKind(V2), V1, V2) |
| U35#(tt, V2) | → | isNat#(V2) | | U103#(tt, M, N) | → | isNatKind#(N) |
| U34#(tt, V1, V2) | → | isNat#(V1) | | isNat#(x(V1, V2)) | → | U31#(isNatKind(V1), V1, V2) |
| isNatKind#(s(V1)) | → | isNatKind#(V1) | | isNat#(x(V1, V2)) | → | isNatKind#(V1) |
| U61#(tt, V2) | → | isNatKind#(V2) | | U102#(tt, M, N) | → | isNat#(N) |
| U15#(tt, V2) | → | isNat#(V2) | | isNat#(plus(V1, V2)) | → | U11#(isNatKind(V1), V1, V2) |
| U11#(tt, V1, V2) | → | U12#(isNatKind(V1), V1, V2) | | U103#(tt, M, N) | → | U104#(isNatKind(N), M, N) |
| U31#(tt, V1, V2) | → | isNatKind#(V1) | | U14#(tt, V1, V2) | → | isNat#(V1) |
| U11#(tt, V1, V2) | → | isNatKind#(V1) | | U22#(tt, V1) | → | U23#(isNat(V1)) |
| U81#(tt, M, N) | → | isNatKind#(M) | | U84#(tt, M, N) | → | T(M) |
| U102#(tt, M, N) | → | U103#(isNat(N), M, N) | | U101#(tt, M, N) | → | isNatKind#(M) |
| U82#(tt, M, N) | → | U83#(isNat(N), M, N) | | U32#(tt, V1, V2) | → | isNatKind#(V2) |
| x#(N, 0) | → | U91#(isNat(N), N) | | U21#(tt, V1) | → | isNatKind#(V1) |
| U33#(tt, V1, V2) | → | isNatKind#(V2) | | U91#(tt, N) | → | isNatKind#(N) |
| isNatKind#(x(V1, V2)) | → | U61#(isNatKind(V1), V2) | | U35#(tt, V2) | → | U36#(isNat(V2)) |
| U61#(tt, V2) | → | U62#(isNatKind(V2)) | | U72#(tt, N) | → | T(N) |
| plus#(N, 0) | → | isNat#(N) | | U71#(tt, N) | → | isNatKind#(N) |
| U12#(tt, V1, V2) | → | U13#(isNatKind(V2), V1, V2) | | U22#(tt, V1) | → | isNat#(V1) |
| U71#(tt, N) | → | U72#(isNatKind(N), N) | | U83#(tt, M, N) | → | U84#(isNatKind(N), M, N) |
| U21#(tt, V1) | → | U22#(isNatKind(V1), V1) | | plus#(N, s(M)) | → | U81#(isNat(M), M, N) |
| U84#(tt, M, N) | → | plus#(N, M) | | plus#(N, s(M)) | → | isNat#(M) |
| U81#(tt, M, N) | → | U82#(isNatKind(M), M, N) | | U14#(tt, V1, V2) | → | U15#(isNat(V1), V2) |
| U32#(tt, V1, V2) | → | U33#(isNatKind(V2), V1, V2) | | isNatKind#(s(V1)) | → | U51#(isNatKind(V1)) |
| isNatKind#(x(V1, V2)) | → | isNatKind#(V1) | | U33#(tt, V1, V2) | → | U34#(isNatKind(V2), V1, V2) |
| x#(N, 0) | → | isNat#(N) | | isNatKind#(plus(V1, V2)) | → | isNatKind#(V1) |
| U82#(tt, M, N) | → | isNat#(N) | | U104#(tt, M, N) | → | T(M) |
| U91#(tt, N) | → | U92#(isNatKind(N)) | | U41#(tt, V2) | → | isNatKind#(V2) |
| U31#(tt, V1, V2) | → | U32#(isNatKind(V1), V1, V2) | | isNat#(plus(V1, V2)) | → | isNatKind#(V1) |
| x#(N, s(M)) | → | isNat#(M) | | U104#(tt, M, N) | → | T(N) |
| U34#(tt, V1, V2) | → | U35#(isNat(V1), V2) | | U84#(tt, M, N) | → | T(N) |
| U104#(tt, M, N) | → | plus#(x(N, M), N) | | U101#(tt, M, N) | → | U102#(isNatKind(M), M, N) |
Rewrite Rules
| U101(tt, M, N) | → | U102(isNatKind(M), M, N) | | U102(tt, M, N) | → | U103(isNat(N), M, N) |
| U103(tt, M, N) | → | U104(isNatKind(N), M, N) | | U104(tt, M, N) | → | plus(x(N, M), N) |
| 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, V1, V2) | → | U32(isNatKind(V1), V1, V2) |
| U32(tt, V1, V2) | → | U33(isNatKind(V2), V1, V2) | | U33(tt, V1, V2) | → | U34(isNatKind(V2), V1, V2) |
| U34(tt, V1, V2) | → | U35(isNat(V1), V2) | | U35(tt, V2) | → | U36(isNat(V2)) |
| U36(tt) | → | tt | | U41(tt, V2) | → | U42(isNatKind(V2)) |
| U42(tt) | → | tt | | U51(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | U62(tt) | → | tt |
| U71(tt, N) | → | U72(isNatKind(N), N) | | U72(tt, N) | → | N |
| U81(tt, M, N) | → | U82(isNatKind(M), M, N) | | U82(tt, M, N) | → | U83(isNat(N), M, N) |
| U83(tt, M, N) | → | U84(isNatKind(N), M, N) | | U84(tt, M, N) | → | s(plus(N, M)) |
| U91(tt, N) | → | U92(isNatKind(N)) | | U92(tt) | → | 0 |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNat(x(V1, V2)) | → | U31(isNatKind(V1), V1, V2) |
| isNatKind(0) | → | tt | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| isNatKind(s(V1)) | → | U51(isNatKind(V1)) | | isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
| plus(N, 0) | → | U71(isNat(N), N) | | plus(N, s(M)) | → | U81(isNat(M), M, N) |
| x(N, 0) | → | U91(isNat(N), N) | | x(N, s(M)) | → | U101(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: U104, isNat, U62, U61, U42, U41, U92, U91, U23, U21, U22, plus, isNatKind, U83, U84, U71, U36, U72, 0, s, U51, U14, tt, U15, U16, U82, U81, U11, U12, U31, U13, U32, U102, U33, U103, U34, U35, U101, x
Strategy
Context-sensitive strategy:
μ(isNatKind) = μ(0) = μ(isNatKind#) = μ(isNat) = μ(T) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U104) = μ(U104#) = μ(U35#) = μ(U41#) = μ(U62) = μ(U61) = μ(U72#) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U103#) = μ(U51#) = μ(U71) = μ(U36) = μ(U42#) = μ(U72) = μ(U71#) = μ(U36#) = μ(U32#) = μ(U15#) = μ(U31) = μ(U32) = μ(U33) = μ(U34) = μ(U35) = μ(U13#) = μ(U91#) = μ(U102#) = μ(U81#) = μ(U23#) = μ(U42) = μ(U92) = μ(U41) = μ(U91) = μ(U84#) = μ(U33#) = μ(U14#) = μ(U101#) = μ(U92#) = μ(U83) = μ(U84) = μ(U82#) = μ(U51) = μ(U14) = μ(s) = μ(U15) = μ(U16) = μ(U82) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = μ(U102) = μ(U103) = μ(U34#) = μ(U101) = {1}
μ(plus) = μ(x#) = μ(plus#) = μ(x) = {1, 2}
The following SCCs where found
| U82#(tt, M, N) → U83#(isNat(N), M, N) | U83#(tt, M, N) → U84#(isNatKind(N), M, N) |
| plus#(N, s(M)) → U81#(isNat(M), M, N) | U84#(tt, M, N) → plus#(N, M) |
| U81#(tt, M, N) → U82#(isNatKind(M), M, N) |
| isNatKind#(s(V1)) → isNatKind#(V1) | isNatKind#(x(V1, V2)) → U61#(isNatKind(V1), V2) |
| isNatKind#(plus(V1, V2)) → isNatKind#(V1) | isNatKind#(plus(V1, V2)) → U41#(isNatKind(V1), V2) |
| U61#(tt, V2) → isNatKind#(V2) | isNatKind#(x(V1, V2)) → isNatKind#(V1) |
| U41#(tt, V2) → isNatKind#(V2) |
| U12#(tt, V1, V2) → U13#(isNatKind(V2), V1, V2) | isNat#(s(V1)) → U21#(isNatKind(V1), V1) |
| U22#(tt, V1) → isNat#(V1) | U21#(tt, V1) → U22#(isNatKind(V1), V1) |
| U13#(tt, V1, V2) → U14#(isNatKind(V2), V1, V2) | U35#(tt, V2) → isNat#(V2) |
| U34#(tt, V1, V2) → isNat#(V1) | U31#(tt, V1, V2) → U32#(isNatKind(V1), V1, V2) |
| isNat#(x(V1, V2)) → U31#(isNatKind(V1), V1, V2) | U14#(tt, V1, V2) → U15#(isNat(V1), V2) |
| U32#(tt, V1, V2) → U33#(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) |
| U34#(tt, V1, V2) → U35#(isNat(V1), V2) | U14#(tt, V1, V2) → isNat#(V1) |
| U33#(tt, V1, V2) → U34#(isNatKind(V2), V1, V2) |
| x#(N, s(M)) → U101#(isNat(M), M, N) | U102#(tt, M, N) → U103#(isNat(N), M, N) |
| U104#(tt, M, N) → x#(N, M) | U103#(tt, M, N) → U104#(isNatKind(N), M, N) |
| U101#(tt, M, N) → U102#(isNatKind(M), M, N) |
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| U12#(tt, V1, V2) | → | U13#(isNatKind(V2), V1, V2) | | isNat#(s(V1)) | → | U21#(isNatKind(V1), V1) |
| U22#(tt, V1) | → | isNat#(V1) | | U35#(tt, V2) | → | isNat#(V2) |
| U13#(tt, V1, V2) | → | U14#(isNatKind(V2), V1, V2) | | U21#(tt, V1) | → | U22#(isNatKind(V1), V1) |
| U34#(tt, V1, V2) | → | isNat#(V1) | | isNat#(x(V1, V2)) | → | U31#(isNatKind(V1), V1, V2) |
| U31#(tt, V1, V2) | → | U32#(isNatKind(V1), V1, V2) | | U14#(tt, V1, V2) | → | U15#(isNat(V1), V2) |
| U32#(tt, V1, V2) | → | U33#(isNatKind(V2), 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) |
| U34#(tt, V1, V2) | → | U35#(isNat(V1), V2) | | U14#(tt, V1, V2) | → | isNat#(V1) |
| U33#(tt, V1, V2) | → | U34#(isNatKind(V2), V1, V2) |
Rewrite Rules
| U101(tt, M, N) | → | U102(isNatKind(M), M, N) | | U102(tt, M, N) | → | U103(isNat(N), M, N) |
| U103(tt, M, N) | → | U104(isNatKind(N), M, N) | | U104(tt, M, N) | → | plus(x(N, M), N) |
| 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, V1, V2) | → | U32(isNatKind(V1), V1, V2) |
| U32(tt, V1, V2) | → | U33(isNatKind(V2), V1, V2) | | U33(tt, V1, V2) | → | U34(isNatKind(V2), V1, V2) |
| U34(tt, V1, V2) | → | U35(isNat(V1), V2) | | U35(tt, V2) | → | U36(isNat(V2)) |
| U36(tt) | → | tt | | U41(tt, V2) | → | U42(isNatKind(V2)) |
| U42(tt) | → | tt | | U51(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | U62(tt) | → | tt |
| U71(tt, N) | → | U72(isNatKind(N), N) | | U72(tt, N) | → | N |
| U81(tt, M, N) | → | U82(isNatKind(M), M, N) | | U82(tt, M, N) | → | U83(isNat(N), M, N) |
| U83(tt, M, N) | → | U84(isNatKind(N), M, N) | | U84(tt, M, N) | → | s(plus(N, M)) |
| U91(tt, N) | → | U92(isNatKind(N)) | | U92(tt) | → | 0 |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNat(x(V1, V2)) | → | U31(isNatKind(V1), V1, V2) |
| isNatKind(0) | → | tt | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| isNatKind(s(V1)) | → | U51(isNatKind(V1)) | | isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
| plus(N, 0) | → | U71(isNat(N), N) | | plus(N, s(M)) | → | U81(isNat(M), M, N) |
| x(N, 0) | → | U91(isNat(N), N) | | x(N, s(M)) | → | U101(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: U104, isNat, U62, U61, U42, U41, U92, U91, U23, U21, U22, plus, isNatKind, U83, U84, U71, U36, U72, 0, s, U51, U14, tt, U15, U16, U82, U81, U11, U12, U31, U13, U32, U102, U33, U103, U34, U35, U101, x
Strategy
Context-sensitive strategy:
μ(isNatKind) = μ(0) = μ(isNatKind#) = μ(isNat) = μ(T) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U104) = μ(U104#) = μ(U35#) = μ(U41#) = μ(U62) = μ(U61) = μ(U72#) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U103#) = μ(U51#) = μ(U71) = μ(U36) = μ(U42#) = μ(U72) = μ(U71#) = μ(U36#) = μ(U32#) = μ(U15#) = μ(U31) = μ(U32) = μ(U33) = μ(U34) = μ(U35) = μ(U13#) = μ(U91#) = μ(U102#) = μ(U81#) = μ(U23#) = μ(U42) = μ(U92) = μ(U41) = μ(U91) = μ(U33#) = μ(U84#) = μ(U14#) = μ(U101#) = μ(U92#) = μ(U83) = μ(U84) = μ(U82#) = μ(s) = μ(U14) = μ(U51) = μ(U15) = μ(U82) = μ(U16) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U102) = μ(U83#) = μ(U103) = μ(U34#) = μ(U101) = {1}
μ(plus) = μ(x#) = μ(plus#) = μ(x) = {1, 2}
Polynomial Interpretation
- 0: 0
- U101(x,y,z): 0
- U102(x,y,z): 0
- U103(x,y,z): 0
- U104(x,y,z): 0
- U11(x,y,z): 0
- U11#(x,y,z): 2z + y + 2
- U12(x,y,z): 0
- U12#(x,y,z): z + y + 2
- U13(x,y,z): 0
- U13#(x,y,z): z + y + 2
- U14(x,y,z): 0
- U14#(x,y,z): z + y
- U15(x,y): 0
- U15#(x,y): y
- U16(x): 0
- U21(x,y): 0
- U21#(x,y): y
- U22(x,y): 0
- U22#(x,y): y
- U23(x): 0
- U31(x,y,z): 0
- U31#(x,y,z): 3z + 3y
- U32(x,y,z): 0
- U32#(x,y,z): 3z + 2y
- U33(x,y,z): 0
- U33#(x,y,z): 2z + 2y
- U34(x,y,z): 0
- U34#(x,y,z): z + 2y
- U35(x,y): 0
- U35#(x,y): y
- U36(x): 0
- U41(x,y): 0
- U42(x): 0
- U51(x): 0
- U61(x,y): 0
- U62(x): 0
- U71(x,y): 0
- U72(x,y): 0
- U81(x,y,z): 0
- U82(x,y,z): 0
- U83(x,y,z): 0
- U84(x,y,z): 0
- U91(x,y): 0
- U92(x): 0
- isNat(x): 0
- isNat#(x): x
- isNatKind(x): 0
- plus(x,y): 2y + x + 2
- s(x): 2x
- tt: 0
- x(x,y): 3y + 3x
Standard Usable rules
| U33(tt, V1, V2) | → | U34(isNatKind(V2), V1, V2) | | isNat(x(V1, V2)) | → | U31(isNatKind(V1), V1, V2) |
| isNatKind(s(V1)) | → | U51(isNatKind(V1)) | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| U15(tt, V2) | → | U16(isNat(V2)) | | isNat(s(V1)) | → | U21(isNatKind(V1), V1) |
| U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) | | U32(tt, V1, V2) | → | U33(isNatKind(V2), V1, V2) |
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | U31(tt, V1, V2) | → | U32(isNatKind(V1), V1, V2) |
| U62(tt) | → | tt | | isNatKind(0) | → | tt |
| U36(tt) | → | tt | | isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
| isNat(0) | → | tt | | U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) |
| U23(tt) | → | tt | | U34(tt, V1, V2) | → | U35(isNat(V1), V2) |
| U14(tt, V1, V2) | → | U15(isNat(V1), V2) | | U35(tt, V2) | → | U36(isNat(V2)) |
| U41(tt, V2) | → | U42(isNatKind(V2)) | | U42(tt) | → | tt |
| U51(tt) | → | tt | | U16(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | 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:
| U13#(tt, V1, V2) | → | U14#(isNatKind(V2), V1, V2) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U12#(tt, V1, V2) | → | U13#(isNatKind(V2), V1, V2) | | isNat#(s(V1)) | → | U21#(isNatKind(V1), V1) |
| U22#(tt, V1) | → | isNat#(V1) | | U35#(tt, V2) | → | isNat#(V2) |
| U21#(tt, V1) | → | U22#(isNatKind(V1), V1) | | U34#(tt, V1, V2) | → | isNat#(V1) |
| isNat#(x(V1, V2)) | → | U31#(isNatKind(V1), V1, V2) | | U31#(tt, V1, V2) | → | U32#(isNatKind(V1), V1, V2) |
| U14#(tt, V1, V2) | → | U15#(isNat(V1), V2) | | U32#(tt, V1, V2) | → | U33#(isNatKind(V2), 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) | | U34#(tt, V1, V2) | → | U35#(isNat(V1), V2) |
| U14#(tt, V1, V2) | → | isNat#(V1) | | U33#(tt, V1, V2) | → | U34#(isNatKind(V2), V1, V2) |
Rewrite Rules
| U101(tt, M, N) | → | U102(isNatKind(M), M, N) | | U102(tt, M, N) | → | U103(isNat(N), M, N) |
| U103(tt, M, N) | → | U104(isNatKind(N), M, N) | | U104(tt, M, N) | → | plus(x(N, M), N) |
| 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, V1, V2) | → | U32(isNatKind(V1), V1, V2) |
| U32(tt, V1, V2) | → | U33(isNatKind(V2), V1, V2) | | U33(tt, V1, V2) | → | U34(isNatKind(V2), V1, V2) |
| U34(tt, V1, V2) | → | U35(isNat(V1), V2) | | U35(tt, V2) | → | U36(isNat(V2)) |
| U36(tt) | → | tt | | U41(tt, V2) | → | U42(isNatKind(V2)) |
| U42(tt) | → | tt | | U51(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | U62(tt) | → | tt |
| U71(tt, N) | → | U72(isNatKind(N), N) | | U72(tt, N) | → | N |
| U81(tt, M, N) | → | U82(isNatKind(M), M, N) | | U82(tt, M, N) | → | U83(isNat(N), M, N) |
| U83(tt, M, N) | → | U84(isNatKind(N), M, N) | | U84(tt, M, N) | → | s(plus(N, M)) |
| U91(tt, N) | → | U92(isNatKind(N)) | | U92(tt) | → | 0 |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNat(x(V1, V2)) | → | U31(isNatKind(V1), V1, V2) |
| isNatKind(0) | → | tt | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| isNatKind(s(V1)) | → | U51(isNatKind(V1)) | | isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
| plus(N, 0) | → | U71(isNat(N), N) | | plus(N, s(M)) | → | U81(isNat(M), M, N) |
| x(N, 0) | → | U91(isNat(N), N) | | x(N, s(M)) | → | U101(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: U104, isNat, U62, U61, U42, U92, U41, U91, U23, U21, U22, plus, isNatKind, U83, U84, U71, U36, U72, 0, s, U51, U14, tt, U15, U82, U16, U81, U11, U12, U13, U31, U102, U32, U103, U33, U34, x, U101, U35
Strategy
Context-sensitive strategy:
μ(isNatKind) = μ(0) = μ(isNatKind#) = μ(isNat) = μ(T) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U104) = μ(U104#) = μ(U35#) = μ(U41#) = μ(U62) = μ(U61) = μ(U72#) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U103#) = μ(U51#) = μ(U71) = μ(U36) = μ(U42#) = μ(U72) = μ(U71#) = μ(U36#) = μ(U32#) = μ(U15#) = μ(U31) = μ(U32) = μ(U33) = μ(U34) = μ(U35) = μ(U13#) = μ(U91#) = μ(U102#) = μ(U81#) = μ(U23#) = μ(U42) = μ(U92) = μ(U41) = μ(U91) = μ(U84#) = μ(U33#) = μ(U14#) = μ(U101#) = μ(U92#) = μ(U83) = μ(U84) = μ(U82#) = μ(U51) = μ(U14) = μ(s) = μ(U15) = μ(U16) = μ(U82) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = μ(U102) = μ(U103) = μ(U34#) = μ(U101) = {1}
μ(plus) = μ(x#) = μ(plus#) = μ(x) = {1, 2}
The following SCCs where found
| U32#(tt, V1, V2) → U33#(isNatKind(V2), V1, V2) | isNat#(s(V1)) → U21#(isNatKind(V1), V1) |
| U22#(tt, V1) → isNat#(V1) | U34#(tt, V1, V2) → U35#(isNat(V1), V2) |
| U21#(tt, V1) → U22#(isNatKind(V1), V1) | U35#(tt, V2) → isNat#(V2) |
| U34#(tt, V1, V2) → isNat#(V1) | isNat#(x(V1, V2)) → U31#(isNatKind(V1), V1, V2) |
| U31#(tt, V1, V2) → U32#(isNatKind(V1), V1, V2) | U33#(tt, V1, V2) → U34#(isNatKind(V2), V1, V2) |
Problem 8: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| U32#(tt, V1, V2) | → | U33#(isNatKind(V2), V1, V2) | | isNat#(s(V1)) | → | U21#(isNatKind(V1), V1) |
| U22#(tt, V1) | → | isNat#(V1) | | U34#(tt, V1, V2) | → | U35#(isNat(V1), V2) |
| U21#(tt, V1) | → | U22#(isNatKind(V1), V1) | | U35#(tt, V2) | → | isNat#(V2) |
| U34#(tt, V1, V2) | → | isNat#(V1) | | isNat#(x(V1, V2)) | → | U31#(isNatKind(V1), V1, V2) |
| U31#(tt, V1, V2) | → | U32#(isNatKind(V1), V1, V2) | | U33#(tt, V1, V2) | → | U34#(isNatKind(V2), V1, V2) |
Rewrite Rules
| U101(tt, M, N) | → | U102(isNatKind(M), M, N) | | U102(tt, M, N) | → | U103(isNat(N), M, N) |
| U103(tt, M, N) | → | U104(isNatKind(N), M, N) | | U104(tt, M, N) | → | plus(x(N, M), N) |
| 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, V1, V2) | → | U32(isNatKind(V1), V1, V2) |
| U32(tt, V1, V2) | → | U33(isNatKind(V2), V1, V2) | | U33(tt, V1, V2) | → | U34(isNatKind(V2), V1, V2) |
| U34(tt, V1, V2) | → | U35(isNat(V1), V2) | | U35(tt, V2) | → | U36(isNat(V2)) |
| U36(tt) | → | tt | | U41(tt, V2) | → | U42(isNatKind(V2)) |
| U42(tt) | → | tt | | U51(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | U62(tt) | → | tt |
| U71(tt, N) | → | U72(isNatKind(N), N) | | U72(tt, N) | → | N |
| U81(tt, M, N) | → | U82(isNatKind(M), M, N) | | U82(tt, M, N) | → | U83(isNat(N), M, N) |
| U83(tt, M, N) | → | U84(isNatKind(N), M, N) | | U84(tt, M, N) | → | s(plus(N, M)) |
| U91(tt, N) | → | U92(isNatKind(N)) | | U92(tt) | → | 0 |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNat(x(V1, V2)) | → | U31(isNatKind(V1), V1, V2) |
| isNatKind(0) | → | tt | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| isNatKind(s(V1)) | → | U51(isNatKind(V1)) | | isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
| plus(N, 0) | → | U71(isNat(N), N) | | plus(N, s(M)) | → | U81(isNat(M), M, N) |
| x(N, 0) | → | U91(isNat(N), N) | | x(N, s(M)) | → | U101(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: U104, isNat, U62, U61, U42, U92, U41, U91, U23, U21, U22, plus, isNatKind, U83, U84, U71, U36, U72, 0, s, U51, U14, tt, U15, U82, U16, U81, U11, U12, U13, U31, U102, U32, U103, U33, U34, x, U101, U35
Strategy
Context-sensitive strategy:
μ(isNatKind) = μ(0) = μ(isNatKind#) = μ(isNat) = μ(T) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U104) = μ(U104#) = μ(U35#) = μ(U41#) = μ(U62) = μ(U61) = μ(U72#) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U103#) = μ(U51#) = μ(U71) = μ(U36) = μ(U42#) = μ(U72) = μ(U71#) = μ(U36#) = μ(U32#) = μ(U15#) = μ(U31) = μ(U32) = μ(U33) = μ(U34) = μ(U35) = μ(U13#) = μ(U91#) = μ(U102#) = μ(U81#) = μ(U23#) = μ(U42) = μ(U92) = μ(U41) = μ(U91) = μ(U33#) = μ(U84#) = μ(U14#) = μ(U101#) = μ(U92#) = μ(U83) = μ(U84) = μ(U82#) = μ(s) = μ(U14) = μ(U51) = μ(U15) = μ(U82) = μ(U16) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U102) = μ(U83#) = μ(U103) = μ(U34#) = μ(U101) = {1}
μ(plus) = μ(x#) = μ(plus#) = μ(x) = {1, 2}
Polynomial Interpretation
- 0: 1
- U101(x,y,z): 0
- U102(x,y,z): 0
- U103(x,y,z): 0
- U104(x,y,z): 0
- U11(x,y,z): x
- U12(x,y,z): x
- U13(x,y,z): 2
- U14(x,y,z): x
- U15(x,y): 2
- U16(x): 2
- U21(x,y): y + x
- U21#(x,y): 2y + x
- U22(x,y): 2
- U22#(x,y): 2y
- U23(x): 2
- U31(x,y,z): 3y
- U31#(x,y,z): 2z + 2y
- U32(x,y,z): 3y
- U32#(x,y,z): 2z + 2y
- U33(x,y,z): 3y
- U33#(x,y,z): 2z + 2y
- U34(x,y,z): 3y
- U34#(x,y,z): 2z + 2y
- U35(x,y): x
- U35#(x,y): 2y
- U36(x): 2
- U41(x,y): x
- U42(x): 2
- U51(x): 2
- U61(x,y): x
- U62(x): x
- U71(x,y): 0
- U72(x,y): 0
- U81(x,y,z): 0
- U82(x,y,z): 0
- U83(x,y,z): 0
- U84(x,y,z): 0
- U91(x,y): 0
- U92(x): 0
- isNat(x): 2x
- isNat#(x): 2x
- isNatKind(x): 2
- plus(x,y): 1
- s(x): x + 1
- tt: 2
- x(x,y): 2y + 3x
Standard Usable rules
| U33(tt, V1, V2) | → | U34(isNatKind(V2), V1, V2) | | isNat(x(V1, V2)) | → | U31(isNatKind(V1), V1, V2) |
| isNatKind(s(V1)) | → | U51(isNatKind(V1)) | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| U15(tt, V2) | → | U16(isNat(V2)) | | isNat(s(V1)) | → | U21(isNatKind(V1), V1) |
| U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) | | U32(tt, V1, V2) | → | U33(isNatKind(V2), V1, V2) |
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | U31(tt, V1, V2) | → | U32(isNatKind(V1), V1, V2) |
| U62(tt) | → | tt | | isNatKind(0) | → | tt |
| U36(tt) | → | tt | | isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
| isNat(0) | → | tt | | U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) |
| U23(tt) | → | tt | | U34(tt, V1, V2) | → | U35(isNat(V1), V2) |
| U14(tt, V1, V2) | → | U15(isNat(V1), V2) | | U35(tt, V2) | → | U36(isNat(V2)) |
| U41(tt, V2) | → | U42(isNatKind(V2)) | | U42(tt) | → | tt |
| U51(tt) | → | tt | | U16(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | 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:
| U21#(tt, V1) | → | U22#(isNatKind(V1), V1) |
Problem 10: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U32#(tt, V1, V2) | → | U33#(isNatKind(V2), V1, V2) | | isNat#(s(V1)) | → | U21#(isNatKind(V1), V1) |
| U22#(tt, V1) | → | isNat#(V1) | | U34#(tt, V1, V2) | → | U35#(isNat(V1), V2) |
| U35#(tt, V2) | → | isNat#(V2) | | U34#(tt, V1, V2) | → | isNat#(V1) |
| U33#(tt, V1, V2) | → | U34#(isNatKind(V2), V1, V2) | | U31#(tt, V1, V2) | → | U32#(isNatKind(V1), V1, V2) |
| isNat#(x(V1, V2)) | → | U31#(isNatKind(V1), V1, V2) |
Rewrite Rules
| U101(tt, M, N) | → | U102(isNatKind(M), M, N) | | U102(tt, M, N) | → | U103(isNat(N), M, N) |
| U103(tt, M, N) | → | U104(isNatKind(N), M, N) | | U104(tt, M, N) | → | plus(x(N, M), N) |
| 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, V1, V2) | → | U32(isNatKind(V1), V1, V2) |
| U32(tt, V1, V2) | → | U33(isNatKind(V2), V1, V2) | | U33(tt, V1, V2) | → | U34(isNatKind(V2), V1, V2) |
| U34(tt, V1, V2) | → | U35(isNat(V1), V2) | | U35(tt, V2) | → | U36(isNat(V2)) |
| U36(tt) | → | tt | | U41(tt, V2) | → | U42(isNatKind(V2)) |
| U42(tt) | → | tt | | U51(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | U62(tt) | → | tt |
| U71(tt, N) | → | U72(isNatKind(N), N) | | U72(tt, N) | → | N |
| U81(tt, M, N) | → | U82(isNatKind(M), M, N) | | U82(tt, M, N) | → | U83(isNat(N), M, N) |
| U83(tt, M, N) | → | U84(isNatKind(N), M, N) | | U84(tt, M, N) | → | s(plus(N, M)) |
| U91(tt, N) | → | U92(isNatKind(N)) | | U92(tt) | → | 0 |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNat(x(V1, V2)) | → | U31(isNatKind(V1), V1, V2) |
| isNatKind(0) | → | tt | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| isNatKind(s(V1)) | → | U51(isNatKind(V1)) | | isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
| plus(N, 0) | → | U71(isNat(N), N) | | plus(N, s(M)) | → | U81(isNat(M), M, N) |
| x(N, 0) | → | U91(isNat(N), N) | | x(N, s(M)) | → | U101(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: U104, isNat, U62, U61, U42, U41, U92, U91, U23, U21, U22, plus, isNatKind, U83, U84, U71, U36, U72, 0, s, U51, U14, tt, U15, U16, U82, U81, U11, U12, U31, U13, U32, U102, U33, U103, U34, U35, U101, x
Strategy
Context-sensitive strategy:
μ(isNatKind) = μ(0) = μ(isNatKind#) = μ(isNat) = μ(T) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U104) = μ(U104#) = μ(U35#) = μ(U41#) = μ(U62) = μ(U61) = μ(U72#) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U103#) = μ(U51#) = μ(U71) = μ(U36) = μ(U42#) = μ(U72) = μ(U71#) = μ(U36#) = μ(U32#) = μ(U15#) = μ(U31) = μ(U32) = μ(U33) = μ(U34) = μ(U35) = μ(U13#) = μ(U91#) = μ(U102#) = μ(U81#) = μ(U23#) = μ(U42) = μ(U92) = μ(U41) = μ(U91) = μ(U84#) = μ(U33#) = μ(U14#) = μ(U101#) = μ(U92#) = μ(U83) = μ(U84) = μ(U82#) = μ(U51) = μ(U14) = μ(s) = μ(U15) = μ(U16) = μ(U82) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = μ(U102) = μ(U103) = μ(U34#) = μ(U101) = {1}
μ(plus) = μ(x#) = μ(plus#) = μ(x) = {1, 2}
The following SCCs where found
| U32#(tt, V1, V2) → U33#(isNatKind(V2), V1, V2) | U34#(tt, V1, V2) → U35#(isNat(V1), V2) |
| U35#(tt, V2) → isNat#(V2) | U34#(tt, V1, V2) → isNat#(V1) |
| U33#(tt, V1, V2) → U34#(isNatKind(V2), V1, V2) | isNat#(x(V1, V2)) → U31#(isNatKind(V1), V1, V2) |
| U31#(tt, V1, V2) → U32#(isNatKind(V1), V1, V2) |
Problem 11: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| U32#(tt, V1, V2) | → | U33#(isNatKind(V2), V1, V2) | | U34#(tt, V1, V2) | → | U35#(isNat(V1), V2) |
| U35#(tt, V2) | → | isNat#(V2) | | U34#(tt, V1, V2) | → | isNat#(V1) |
| U33#(tt, V1, V2) | → | U34#(isNatKind(V2), V1, V2) | | isNat#(x(V1, V2)) | → | U31#(isNatKind(V1), V1, V2) |
| U31#(tt, V1, V2) | → | U32#(isNatKind(V1), V1, V2) |
Rewrite Rules
| U101(tt, M, N) | → | U102(isNatKind(M), M, N) | | U102(tt, M, N) | → | U103(isNat(N), M, N) |
| U103(tt, M, N) | → | U104(isNatKind(N), M, N) | | U104(tt, M, N) | → | plus(x(N, M), N) |
| 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, V1, V2) | → | U32(isNatKind(V1), V1, V2) |
| U32(tt, V1, V2) | → | U33(isNatKind(V2), V1, V2) | | U33(tt, V1, V2) | → | U34(isNatKind(V2), V1, V2) |
| U34(tt, V1, V2) | → | U35(isNat(V1), V2) | | U35(tt, V2) | → | U36(isNat(V2)) |
| U36(tt) | → | tt | | U41(tt, V2) | → | U42(isNatKind(V2)) |
| U42(tt) | → | tt | | U51(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | U62(tt) | → | tt |
| U71(tt, N) | → | U72(isNatKind(N), N) | | U72(tt, N) | → | N |
| U81(tt, M, N) | → | U82(isNatKind(M), M, N) | | U82(tt, M, N) | → | U83(isNat(N), M, N) |
| U83(tt, M, N) | → | U84(isNatKind(N), M, N) | | U84(tt, M, N) | → | s(plus(N, M)) |
| U91(tt, N) | → | U92(isNatKind(N)) | | U92(tt) | → | 0 |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNat(x(V1, V2)) | → | U31(isNatKind(V1), V1, V2) |
| isNatKind(0) | → | tt | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| isNatKind(s(V1)) | → | U51(isNatKind(V1)) | | isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
| plus(N, 0) | → | U71(isNat(N), N) | | plus(N, s(M)) | → | U81(isNat(M), M, N) |
| x(N, 0) | → | U91(isNat(N), N) | | x(N, s(M)) | → | U101(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: U104, isNat, U62, U61, U42, U41, U92, U91, U23, U21, U22, plus, isNatKind, U83, U84, U71, U36, U72, 0, s, U51, U14, tt, U15, U16, U82, U81, U11, U12, U31, U13, U32, U102, U33, U103, U34, U35, U101, x
Strategy
Context-sensitive strategy:
μ(isNatKind) = μ(0) = μ(isNatKind#) = μ(isNat) = μ(T) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U104) = μ(U104#) = μ(U35#) = μ(U41#) = μ(U62) = μ(U61) = μ(U72#) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U103#) = μ(U51#) = μ(U71) = μ(U36) = μ(U42#) = μ(U72) = μ(U71#) = μ(U36#) = μ(U32#) = μ(U15#) = μ(U31) = μ(U32) = μ(U33) = μ(U34) = μ(U35) = μ(U13#) = μ(U91#) = μ(U102#) = μ(U81#) = μ(U23#) = μ(U42) = μ(U92) = μ(U41) = μ(U91) = μ(U33#) = μ(U84#) = μ(U14#) = μ(U101#) = μ(U92#) = μ(U83) = μ(U84) = μ(U82#) = μ(s) = μ(U14) = μ(U51) = μ(U15) = μ(U82) = μ(U16) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U102) = μ(U83#) = μ(U103) = μ(U34#) = μ(U101) = {1}
μ(plus) = μ(x#) = μ(plus#) = μ(x) = {1, 2}
Polynomial Interpretation
- 0: 0
- U101(x,y,z): 0
- U102(x,y,z): 0
- U103(x,y,z): 0
- U104(x,y,z): 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,z): 2z + 2y + 2
- U31#(x,y,z): 2z + 2y
- U32(x,y,z): 2z + 2y + 1
- U32#(x,y,z): 2z + 2y
- U33(x,y,z): 2z + 2y
- U33#(x,y,z): 2z + 2y
- U34(x,y,z): 2z + 2y
- U34#(x,y,z): 2z + 2y
- U35(x,y): 2y
- U35#(x,y): 2y
- U36(x): 0
- U41(x,y): 0
- U42(x): 0
- U51(x): 0
- U61(x,y): 0
- U62(x): 0
- U71(x,y): 0
- U72(x,y): 0
- U81(x,y,z): 0
- U82(x,y,z): 0
- U83(x,y,z): 0
- U84(x,y,z): 0
- U91(x,y): 0
- U92(x): 0
- isNat(x): 2x
- isNat#(x): 2x
- isNatKind(x): 0
- plus(x,y): 0
- s(x): 0
- tt: 0
- x(x,y): y + x + 1
Standard Usable rules
| U33(tt, V1, V2) | → | U34(isNatKind(V2), V1, V2) | | isNat(x(V1, V2)) | → | U31(isNatKind(V1), V1, V2) |
| isNatKind(s(V1)) | → | U51(isNatKind(V1)) | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| U15(tt, V2) | → | U16(isNat(V2)) | | isNat(s(V1)) | → | U21(isNatKind(V1), V1) |
| U12(tt, V1, V2) | → | U13(isNatKind(V2), V1, V2) | | U32(tt, V1, V2) | → | U33(isNatKind(V2), V1, V2) |
| U11(tt, V1, V2) | → | U12(isNatKind(V1), V1, V2) | | U31(tt, V1, V2) | → | U32(isNatKind(V1), V1, V2) |
| U62(tt) | → | tt | | isNatKind(0) | → | tt |
| U36(tt) | → | tt | | isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
| isNat(0) | → | tt | | U13(tt, V1, V2) | → | U14(isNatKind(V2), V1, V2) |
| U23(tt) | → | tt | | U34(tt, V1, V2) | → | U35(isNat(V1), V2) |
| U14(tt, V1, V2) | → | U15(isNat(V1), V2) | | U35(tt, V2) | → | U36(isNat(V2)) |
| U41(tt, V2) | → | U42(isNatKind(V2)) | | U42(tt) | → | tt |
| U51(tt) | → | tt | | U16(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | 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:
| isNat#(x(V1, V2)) | → | U31#(isNatKind(V1), V1, V2) |
Problem 12: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U32#(tt, V1, V2) | → | U33#(isNatKind(V2), V1, V2) | | U34#(tt, V1, V2) | → | U35#(isNat(V1), V2) |
| U35#(tt, V2) | → | isNat#(V2) | | U34#(tt, V1, V2) | → | isNat#(V1) |
| U31#(tt, V1, V2) | → | U32#(isNatKind(V1), V1, V2) | | U33#(tt, V1, V2) | → | U34#(isNatKind(V2), V1, V2) |
Rewrite Rules
| U101(tt, M, N) | → | U102(isNatKind(M), M, N) | | U102(tt, M, N) | → | U103(isNat(N), M, N) |
| U103(tt, M, N) | → | U104(isNatKind(N), M, N) | | U104(tt, M, N) | → | plus(x(N, M), N) |
| 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, V1, V2) | → | U32(isNatKind(V1), V1, V2) |
| U32(tt, V1, V2) | → | U33(isNatKind(V2), V1, V2) | | U33(tt, V1, V2) | → | U34(isNatKind(V2), V1, V2) |
| U34(tt, V1, V2) | → | U35(isNat(V1), V2) | | U35(tt, V2) | → | U36(isNat(V2)) |
| U36(tt) | → | tt | | U41(tt, V2) | → | U42(isNatKind(V2)) |
| U42(tt) | → | tt | | U51(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | U62(tt) | → | tt |
| U71(tt, N) | → | U72(isNatKind(N), N) | | U72(tt, N) | → | N |
| U81(tt, M, N) | → | U82(isNatKind(M), M, N) | | U82(tt, M, N) | → | U83(isNat(N), M, N) |
| U83(tt, M, N) | → | U84(isNatKind(N), M, N) | | U84(tt, M, N) | → | s(plus(N, M)) |
| U91(tt, N) | → | U92(isNatKind(N)) | | U92(tt) | → | 0 |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNat(x(V1, V2)) | → | U31(isNatKind(V1), V1, V2) |
| isNatKind(0) | → | tt | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| isNatKind(s(V1)) | → | U51(isNatKind(V1)) | | isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
| plus(N, 0) | → | U71(isNat(N), N) | | plus(N, s(M)) | → | U81(isNat(M), M, N) |
| x(N, 0) | → | U91(isNat(N), N) | | x(N, s(M)) | → | U101(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: U104, isNat, U62, U61, U42, U92, U41, U91, U23, U21, U22, plus, isNatKind, U83, U84, U71, U36, U72, 0, s, U51, U14, tt, U15, U82, U16, U81, U11, U12, U13, U31, U102, U32, U103, U33, U34, x, U101, U35
Strategy
Context-sensitive strategy:
μ(isNatKind) = μ(0) = μ(isNatKind#) = μ(isNat) = μ(T) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U104) = μ(U104#) = μ(U35#) = μ(U41#) = μ(U62) = μ(U61) = μ(U72#) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U103#) = μ(U51#) = μ(U71) = μ(U36) = μ(U42#) = μ(U72) = μ(U71#) = μ(U36#) = μ(U32#) = μ(U15#) = μ(U31) = μ(U32) = μ(U33) = μ(U34) = μ(U35) = μ(U13#) = μ(U91#) = μ(U102#) = μ(U81#) = μ(U23#) = μ(U42) = μ(U92) = μ(U41) = μ(U91) = μ(U84#) = μ(U33#) = μ(U14#) = μ(U101#) = μ(U92#) = μ(U83) = μ(U84) = μ(U82#) = μ(U51) = μ(U14) = μ(s) = μ(U15) = μ(U16) = μ(U82) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = μ(U102) = μ(U103) = μ(U34#) = μ(U101) = {1}
μ(plus) = μ(x#) = μ(plus#) = μ(x) = {1, 2}
There are no SCCs!
Problem 5: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNatKind#(s(V1)) | → | isNatKind#(V1) | | isNatKind#(x(V1, V2)) | → | U61#(isNatKind(V1), V2) |
| isNatKind#(plus(V1, V2)) | → | isNatKind#(V1) | | isNatKind#(plus(V1, V2)) | → | U41#(isNatKind(V1), V2) |
| U61#(tt, V2) | → | isNatKind#(V2) | | isNatKind#(x(V1, V2)) | → | isNatKind#(V1) |
| U41#(tt, V2) | → | isNatKind#(V2) |
Rewrite Rules
| U101(tt, M, N) | → | U102(isNatKind(M), M, N) | | U102(tt, M, N) | → | U103(isNat(N), M, N) |
| U103(tt, M, N) | → | U104(isNatKind(N), M, N) | | U104(tt, M, N) | → | plus(x(N, M), N) |
| 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, V1, V2) | → | U32(isNatKind(V1), V1, V2) |
| U32(tt, V1, V2) | → | U33(isNatKind(V2), V1, V2) | | U33(tt, V1, V2) | → | U34(isNatKind(V2), V1, V2) |
| U34(tt, V1, V2) | → | U35(isNat(V1), V2) | | U35(tt, V2) | → | U36(isNat(V2)) |
| U36(tt) | → | tt | | U41(tt, V2) | → | U42(isNatKind(V2)) |
| U42(tt) | → | tt | | U51(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | U62(tt) | → | tt |
| U71(tt, N) | → | U72(isNatKind(N), N) | | U72(tt, N) | → | N |
| U81(tt, M, N) | → | U82(isNatKind(M), M, N) | | U82(tt, M, N) | → | U83(isNat(N), M, N) |
| U83(tt, M, N) | → | U84(isNatKind(N), M, N) | | U84(tt, M, N) | → | s(plus(N, M)) |
| U91(tt, N) | → | U92(isNatKind(N)) | | U92(tt) | → | 0 |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNat(x(V1, V2)) | → | U31(isNatKind(V1), V1, V2) |
| isNatKind(0) | → | tt | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| isNatKind(s(V1)) | → | U51(isNatKind(V1)) | | isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
| plus(N, 0) | → | U71(isNat(N), N) | | plus(N, s(M)) | → | U81(isNat(M), M, N) |
| x(N, 0) | → | U91(isNat(N), N) | | x(N, s(M)) | → | U101(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: U104, isNat, U62, U61, U42, U41, U92, U91, U23, U21, U22, plus, isNatKind, U83, U84, U71, U36, U72, 0, s, U51, U14, tt, U15, U16, U82, U81, U11, U12, U31, U13, U32, U102, U33, U103, U34, U35, U101, x
Strategy
Context-sensitive strategy:
μ(isNatKind) = μ(0) = μ(isNatKind#) = μ(isNat) = μ(T) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U104) = μ(U104#) = μ(U35#) = μ(U41#) = μ(U62) = μ(U61) = μ(U72#) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U103#) = μ(U51#) = μ(U71) = μ(U36) = μ(U42#) = μ(U72) = μ(U71#) = μ(U36#) = μ(U32#) = μ(U15#) = μ(U31) = μ(U32) = μ(U33) = μ(U34) = μ(U35) = μ(U13#) = μ(U91#) = μ(U102#) = μ(U81#) = μ(U23#) = μ(U42) = μ(U92) = μ(U41) = μ(U91) = μ(U33#) = μ(U84#) = μ(U14#) = μ(U101#) = μ(U92#) = μ(U83) = μ(U84) = μ(U82#) = μ(s) = μ(U14) = μ(U51) = μ(U15) = μ(U82) = μ(U16) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U102) = μ(U83#) = μ(U103) = μ(U34#) = μ(U101) = {1}
μ(plus) = μ(x#) = μ(plus#) = μ(x) = {1, 2}
Polynomial Interpretation
- 0: 1
- U101(x,y,z): 0
- U102(x,y,z): 0
- U103(x,y,z): 0
- U104(x,y,z): 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,z): 0
- U32(x,y,z): 0
- U33(x,y,z): 0
- U34(x,y,z): 0
- U35(x,y): 0
- U36(x): 0
- U41(x,y): x
- U41#(x,y): 2y + x
- U42(x): 1
- U51(x): x
- U61(x,y): 2x
- U61#(x,y): 2y
- U62(x): 1
- U71(x,y): 0
- U72(x,y): 0
- U81(x,y,z): 0
- U82(x,y,z): 0
- U83(x,y,z): 0
- U84(x,y,z): 0
- U91(x,y): 0
- U92(x): 0
- isNat(x): 0
- isNatKind(x): 2x
- isNatKind#(x): 2x
- plus(x,y): y + x
- s(x): 3x
- tt: 1
- x(x,y): y + 2x
Standard Usable rules
| U42(tt) | → | tt | | U51(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | isNatKind(s(V1)) | → | U51(isNatKind(V1)) |
| U62(tt) | → | tt | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| U41(tt, V2) | → | U42(isNatKind(V2)) | | isNatKind(0) | → | tt |
| isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U41#(tt, V2) | → | isNatKind#(V2) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isNatKind#(x(V1, V2)) | → | U61#(isNatKind(V1), V2) | | isNatKind#(s(V1)) | → | isNatKind#(V1) |
| isNatKind#(plus(V1, V2)) | → | isNatKind#(V1) | | isNatKind#(plus(V1, V2)) | → | U41#(isNatKind(V1), V2) |
| U61#(tt, V2) | → | isNatKind#(V2) | | isNatKind#(x(V1, V2)) | → | isNatKind#(V1) |
Rewrite Rules
| U101(tt, M, N) | → | U102(isNatKind(M), M, N) | | U102(tt, M, N) | → | U103(isNat(N), M, N) |
| U103(tt, M, N) | → | U104(isNatKind(N), M, N) | | U104(tt, M, N) | → | plus(x(N, M), N) |
| 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, V1, V2) | → | U32(isNatKind(V1), V1, V2) |
| U32(tt, V1, V2) | → | U33(isNatKind(V2), V1, V2) | | U33(tt, V1, V2) | → | U34(isNatKind(V2), V1, V2) |
| U34(tt, V1, V2) | → | U35(isNat(V1), V2) | | U35(tt, V2) | → | U36(isNat(V2)) |
| U36(tt) | → | tt | | U41(tt, V2) | → | U42(isNatKind(V2)) |
| U42(tt) | → | tt | | U51(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | U62(tt) | → | tt |
| U71(tt, N) | → | U72(isNatKind(N), N) | | U72(tt, N) | → | N |
| U81(tt, M, N) | → | U82(isNatKind(M), M, N) | | U82(tt, M, N) | → | U83(isNat(N), M, N) |
| U83(tt, M, N) | → | U84(isNatKind(N), M, N) | | U84(tt, M, N) | → | s(plus(N, M)) |
| U91(tt, N) | → | U92(isNatKind(N)) | | U92(tt) | → | 0 |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNat(x(V1, V2)) | → | U31(isNatKind(V1), V1, V2) |
| isNatKind(0) | → | tt | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| isNatKind(s(V1)) | → | U51(isNatKind(V1)) | | isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
| plus(N, 0) | → | U71(isNat(N), N) | | plus(N, s(M)) | → | U81(isNat(M), M, N) |
| x(N, 0) | → | U91(isNat(N), N) | | x(N, s(M)) | → | U101(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: U104, isNat, U62, U61, U42, U92, U41, U91, U23, U21, U22, plus, isNatKind, U83, U84, U71, U36, U72, 0, s, U51, U14, tt, U15, U82, U16, U81, U11, U12, U13, U31, U102, U32, U103, U33, U34, x, U101, U35
Strategy
Context-sensitive strategy:
μ(isNatKind) = μ(0) = μ(isNatKind#) = μ(isNat) = μ(T) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U104) = μ(U104#) = μ(U35#) = μ(U41#) = μ(U62) = μ(U61) = μ(U72#) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U103#) = μ(U51#) = μ(U71) = μ(U36) = μ(U42#) = μ(U72) = μ(U71#) = μ(U36#) = μ(U32#) = μ(U15#) = μ(U31) = μ(U32) = μ(U33) = μ(U34) = μ(U35) = μ(U13#) = μ(U91#) = μ(U102#) = μ(U81#) = μ(U23#) = μ(U42) = μ(U92) = μ(U41) = μ(U91) = μ(U84#) = μ(U33#) = μ(U14#) = μ(U101#) = μ(U92#) = μ(U83) = μ(U84) = μ(U82#) = μ(U51) = μ(U14) = μ(s) = μ(U15) = μ(U16) = μ(U82) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = μ(U102) = μ(U103) = μ(U34#) = μ(U101) = {1}
μ(plus) = μ(x#) = μ(plus#) = μ(x) = {1, 2}
The following SCCs where found
| isNatKind#(x(V1, V2)) → U61#(isNatKind(V1), V2) | isNatKind#(s(V1)) → isNatKind#(V1) |
| isNatKind#(plus(V1, V2)) → isNatKind#(V1) | U61#(tt, V2) → isNatKind#(V2) |
| isNatKind#(x(V1, V2)) → isNatKind#(V1) |
Problem 9: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNatKind#(x(V1, V2)) | → | U61#(isNatKind(V1), V2) | | isNatKind#(s(V1)) | → | isNatKind#(V1) |
| isNatKind#(plus(V1, V2)) | → | isNatKind#(V1) | | U61#(tt, V2) | → | isNatKind#(V2) |
| isNatKind#(x(V1, V2)) | → | isNatKind#(V1) |
Rewrite Rules
| U101(tt, M, N) | → | U102(isNatKind(M), M, N) | | U102(tt, M, N) | → | U103(isNat(N), M, N) |
| U103(tt, M, N) | → | U104(isNatKind(N), M, N) | | U104(tt, M, N) | → | plus(x(N, M), N) |
| 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, V1, V2) | → | U32(isNatKind(V1), V1, V2) |
| U32(tt, V1, V2) | → | U33(isNatKind(V2), V1, V2) | | U33(tt, V1, V2) | → | U34(isNatKind(V2), V1, V2) |
| U34(tt, V1, V2) | → | U35(isNat(V1), V2) | | U35(tt, V2) | → | U36(isNat(V2)) |
| U36(tt) | → | tt | | U41(tt, V2) | → | U42(isNatKind(V2)) |
| U42(tt) | → | tt | | U51(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | U62(tt) | → | tt |
| U71(tt, N) | → | U72(isNatKind(N), N) | | U72(tt, N) | → | N |
| U81(tt, M, N) | → | U82(isNatKind(M), M, N) | | U82(tt, M, N) | → | U83(isNat(N), M, N) |
| U83(tt, M, N) | → | U84(isNatKind(N), M, N) | | U84(tt, M, N) | → | s(plus(N, M)) |
| U91(tt, N) | → | U92(isNatKind(N)) | | U92(tt) | → | 0 |
| isNat(0) | → | tt | | isNat(plus(V1, V2)) | → | U11(isNatKind(V1), V1, V2) |
| isNat(s(V1)) | → | U21(isNatKind(V1), V1) | | isNat(x(V1, V2)) | → | U31(isNatKind(V1), V1, V2) |
| isNatKind(0) | → | tt | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| isNatKind(s(V1)) | → | U51(isNatKind(V1)) | | isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
| plus(N, 0) | → | U71(isNat(N), N) | | plus(N, s(M)) | → | U81(isNat(M), M, N) |
| x(N, 0) | → | U91(isNat(N), N) | | x(N, s(M)) | → | U101(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: U104, isNat, U62, U61, U42, U92, U41, U91, U23, U21, U22, plus, isNatKind, U83, U84, U71, U36, U72, 0, s, U51, U14, tt, U15, U82, U16, U81, U11, U12, U13, U31, U102, U32, U103, U33, U34, x, U101, U35
Strategy
Context-sensitive strategy:
μ(isNatKind) = μ(0) = μ(isNatKind#) = μ(isNat) = μ(T) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U104) = μ(U104#) = μ(U35#) = μ(U41#) = μ(U62) = μ(U61) = μ(U72#) = μ(U16#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U103#) = μ(U51#) = μ(U71) = μ(U36) = μ(U42#) = μ(U72) = μ(U71#) = μ(U36#) = μ(U32#) = μ(U15#) = μ(U31) = μ(U32) = μ(U33) = μ(U34) = μ(U35) = μ(U13#) = μ(U91#) = μ(U102#) = μ(U81#) = μ(U23#) = μ(U42) = μ(U92) = μ(U41) = μ(U91) = μ(U33#) = μ(U84#) = μ(U14#) = μ(U101#) = μ(U92#) = μ(U83) = μ(U84) = μ(U82#) = μ(s) = μ(U14) = μ(U51) = μ(U15) = μ(U82) = μ(U16) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U102) = μ(U83#) = μ(U103) = μ(U34#) = μ(U101) = {1}
μ(plus) = μ(x#) = μ(plus#) = μ(x) = {1, 2}
Polynomial Interpretation
- 0: 1
- U101(x,y,z): 0
- U102(x,y,z): 0
- U103(x,y,z): 0
- U104(x,y,z): 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,z): 0
- U32(x,y,z): 0
- U33(x,y,z): 0
- U34(x,y,z): 0
- U35(x,y): 0
- U36(x): 0
- U41(x,y): 2y
- U42(x): x
- U51(x): 2
- U61(x,y): 2y + x
- U61#(x,y): 3y + x + 1
- U62(x): x
- U71(x,y): 0
- U72(x,y): 0
- U81(x,y,z): 0
- U82(x,y,z): 0
- U83(x,y,z): 0
- U84(x,y,z): 0
- U91(x,y): 0
- U92(x): 0
- isNat(x): 0
- isNatKind(x): 2x
- isNatKind#(x): 2x
- plus(x,y): y + 2x + 1
- s(x): 2x + 1
- tt: 2
- x(x,y): 2y + 2x + 1
Standard Usable rules
| U42(tt) | → | tt | | U51(tt) | → | tt |
| U61(tt, V2) | → | U62(isNatKind(V2)) | | isNatKind(s(V1)) | → | U51(isNatKind(V1)) |
| U62(tt) | → | tt | | isNatKind(plus(V1, V2)) | → | U41(isNatKind(V1), V2) |
| U41(tt, V2) | → | U42(isNatKind(V2)) | | isNatKind(0) | → | tt |
| isNatKind(x(V1, V2)) | → | U61(isNatKind(V1), V2) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isNatKind#(s(V1)) | → | isNatKind#(V1) | | isNatKind#(x(V1, V2)) | → | U61#(isNatKind(V1), V2) |
| isNatKind#(plus(V1, V2)) | → | isNatKind#(V1) | | U61#(tt, V2) | → | isNatKind#(V2) |
| isNatKind#(x(V1, V2)) | → | isNatKind#(V1) |