TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60266 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (1832ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (535ms).
| | – Problem 5 was processed with processor DependencyGraph (33ms).
| | | – Problem 6 was processed with processor PolynomialLinearRange4 (14ms).
| | | | – Problem 7 was processed with processor PolynomialLinearRange4 (9ms).
| – Problem 3 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (3ms), PolynomialOrderingProcessor (0ms), DependencyGraph (5ms), PolynomialLinearRange4 (406ms), DependencyGraph (4ms), PolynomialLinearRange4 (336ms), DependencyGraph (3ms), PolynomialLinearRange4 (276ms), DependencyGraph (13ms), PolynomialLinearRange4 (350ms), DependencyGraph (2ms), ReductionPairSAT (12611ms), DependencyGraph (2ms), SizeChangePrinciple (timeout)].
| – Problem 4 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (4ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (5ms), PolynomialOrderingProcessor (0ms), DependencyGraph (4ms), PolynomialLinearRange4 (332ms), DependencyGraph (5ms), PolynomialLinearRange4 (233ms), DependencyGraph (3ms), PolynomialLinearRange4 (194ms), DependencyGraph (3ms), PolynomialLinearRange4 (168ms), DependencyGraph (4ms), ReductionPairSAT (6025ms), DependencyGraph (3ms)].
The following open problems remain:
Open Dependency Pair Problem 3
Dependency Pairs
| U201#(tt, N, X, XS) | → | U202#(isNatural(X), N, X, XS) | | splitAt#(s(N), cons(X, XS)) | → | U201#(isNatural(N), N, X, XS) |
| U203#(tt, N, X, XS) | → | splitAt#(N, XS) | | U202#(tt, N, X, XS) | → | U203#(isLNat(XS), N, X, XS) |
Rewrite Rules
| U101(tt, V2) | → | U102(isLNat(V2)) | | U102(tt) | → | tt |
| U11(tt, N, XS) | → | U12(isLNat(XS), N, XS) | | U111(tt) | → | tt |
| U12(tt, N, XS) | → | snd(splitAt(N, XS)) | | U121(tt) | → | tt |
| U131(tt, V2) | → | U132(isLNat(V2)) | | U132(tt) | → | tt |
| U141(tt, V2) | → | U142(isLNat(V2)) | | U142(tt) | → | tt |
| U151(tt, V2) | → | U152(isLNat(V2)) | | U152(tt) | → | tt |
| U161(tt, N) | → | cons(N, natsFrom(s(N))) | | U171(tt, N, XS) | → | U172(isLNat(XS), N, XS) |
| U172(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | U182(isLNat(Y), Y) |
| U182(tt, Y) | → | Y | | U191(tt, XS) | → | pair(nil, XS) |
| U201(tt, N, X, XS) | → | U202(isNatural(X), N, X, XS) | | U202(tt, N, X, XS) | → | U203(isLNat(XS), N, X, XS) |
| U203(tt, N, X, XS) | → | U204(splitAt(N, XS), X) | | U204(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) |
| U21(tt, X, Y) | → | U22(isLNat(Y), X) | | U211(tt, XS) | → | U212(isLNat(XS), XS) |
| U212(tt, XS) | → | XS | | U22(tt, X) | → | X |
| U221(tt, N, XS) | → | U222(isLNat(XS), N, XS) | | U222(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N, XS) | → | U32(isLNat(XS), N) | | U32(tt, N) | → | N |
| U41(tt, V2) | → | U42(isLNat(V2)) | | U42(tt) | → | tt |
| U51(tt, V2) | → | U52(isLNat(V2)) | | U52(tt) | → | tt |
| U61(tt) | → | tt | | U71(tt) | → | tt |
| U81(tt) | → | tt | | U91(tt) | → | tt |
| afterNth(N, XS) | → | U11(isNatural(N), N, XS) | | fst(pair(X, Y)) | → | U21(isLNat(X), X, Y) |
| head(cons(N, XS)) | → | U31(isNatural(N), N, XS) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(isNatural(V1), V2) | | isLNat(cons(V1, V2)) | → | U51(isNatural(V1), V2) |
| isLNat(fst(V1)) | → | U61(isPLNat(V1)) | | isLNat(natsFrom(V1)) | → | U71(isNatural(V1)) |
| isLNat(snd(V1)) | → | U81(isPLNat(V1)) | | isLNat(tail(V1)) | → | U91(isLNat(V1)) |
| isLNat(take(V1, V2)) | → | U101(isNatural(V1), V2) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNat(V1)) | | isNatural(s(V1)) | → | U121(isNatural(V1)) |
| isNatural(sel(V1, V2)) | → | U131(isNatural(V1), V2) | | isPLNat(pair(V1, V2)) | → | U141(isLNat(V1), V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(isNatural(V1), V2) | | natsFrom(N) | → | U161(isNatural(N), N) |
| sel(N, XS) | → | U171(isNatural(N), N, XS) | | snd(pair(X, Y)) | → | U181(isLNat(X), Y) |
| splitAt(0, XS) | → | U191(isLNat(XS), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(isNatural(N), N, X, XS) |
| tail(cons(N, XS)) | → | U211(isNatural(N), XS) | | take(N, XS) | → | U221(isNatural(N), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U204, U203, fst, U111, U61, U211, U212, head, U21, U22, U151, isPLNat, U152, tail, U191, U71, 0, U121, U221, isLNat, U222, U31, U32, U181, U182, pair, isNatural, U132, U131, U42, U41, U91, cons, snd, U171, U172, splitAt, U201, U142, U202, U141, s, U51, tt, take, U81, U52, U11, U12, afterNth, U102, sel, U101, nil
Open Dependency Pair Problem 4
Dependency Pairs
| T(natsFrom(x_1)) | → | T(x_1) | | natsFrom#(N) | → | U161#(isNatural(N), N) |
| T(s(x_1)) | → | T(x_1) | | T(natsFrom(s(N))) | → | natsFrom#(s(N)) |
| U161#(tt, N) | → | T(N) |
Rewrite Rules
| U101(tt, V2) | → | U102(isLNat(V2)) | | U102(tt) | → | tt |
| U11(tt, N, XS) | → | U12(isLNat(XS), N, XS) | | U111(tt) | → | tt |
| U12(tt, N, XS) | → | snd(splitAt(N, XS)) | | U121(tt) | → | tt |
| U131(tt, V2) | → | U132(isLNat(V2)) | | U132(tt) | → | tt |
| U141(tt, V2) | → | U142(isLNat(V2)) | | U142(tt) | → | tt |
| U151(tt, V2) | → | U152(isLNat(V2)) | | U152(tt) | → | tt |
| U161(tt, N) | → | cons(N, natsFrom(s(N))) | | U171(tt, N, XS) | → | U172(isLNat(XS), N, XS) |
| U172(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | U182(isLNat(Y), Y) |
| U182(tt, Y) | → | Y | | U191(tt, XS) | → | pair(nil, XS) |
| U201(tt, N, X, XS) | → | U202(isNatural(X), N, X, XS) | | U202(tt, N, X, XS) | → | U203(isLNat(XS), N, X, XS) |
| U203(tt, N, X, XS) | → | U204(splitAt(N, XS), X) | | U204(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) |
| U21(tt, X, Y) | → | U22(isLNat(Y), X) | | U211(tt, XS) | → | U212(isLNat(XS), XS) |
| U212(tt, XS) | → | XS | | U22(tt, X) | → | X |
| U221(tt, N, XS) | → | U222(isLNat(XS), N, XS) | | U222(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N, XS) | → | U32(isLNat(XS), N) | | U32(tt, N) | → | N |
| U41(tt, V2) | → | U42(isLNat(V2)) | | U42(tt) | → | tt |
| U51(tt, V2) | → | U52(isLNat(V2)) | | U52(tt) | → | tt |
| U61(tt) | → | tt | | U71(tt) | → | tt |
| U81(tt) | → | tt | | U91(tt) | → | tt |
| afterNth(N, XS) | → | U11(isNatural(N), N, XS) | | fst(pair(X, Y)) | → | U21(isLNat(X), X, Y) |
| head(cons(N, XS)) | → | U31(isNatural(N), N, XS) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(isNatural(V1), V2) | | isLNat(cons(V1, V2)) | → | U51(isNatural(V1), V2) |
| isLNat(fst(V1)) | → | U61(isPLNat(V1)) | | isLNat(natsFrom(V1)) | → | U71(isNatural(V1)) |
| isLNat(snd(V1)) | → | U81(isPLNat(V1)) | | isLNat(tail(V1)) | → | U91(isLNat(V1)) |
| isLNat(take(V1, V2)) | → | U101(isNatural(V1), V2) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNat(V1)) | | isNatural(s(V1)) | → | U121(isNatural(V1)) |
| isNatural(sel(V1, V2)) | → | U131(isNatural(V1), V2) | | isPLNat(pair(V1, V2)) | → | U141(isLNat(V1), V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(isNatural(V1), V2) | | natsFrom(N) | → | U161(isNatural(N), N) |
| sel(N, XS) | → | U171(isNatural(N), N, XS) | | snd(pair(X, Y)) | → | U181(isLNat(X), Y) |
| splitAt(0, XS) | → | U191(isLNat(XS), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(isNatural(N), N, X, XS) |
| tail(cons(N, XS)) | → | U211(isNatural(N), XS) | | take(N, XS) | → | U221(isNatural(N), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U204, U203, fst, U111, U61, U211, U212, head, U21, U22, U151, isPLNat, U152, tail, U191, U71, 0, U121, U221, isLNat, U222, U31, U32, U181, U182, pair, isNatural, U132, U131, U42, U41, U91, cons, snd, U171, U172, splitAt, U201, U142, U202, U141, s, U51, tt, take, U81, U52, U11, U12, afterNth, U102, sel, U101, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U11#(tt, N, XS) | → | isLNat#(XS) | | U22#(tt, X) | → | T(X) |
| splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | | U21#(tt, X, Y) | → | U22#(isLNat(Y), X) |
| U182#(tt, Y) | → | T(Y) | | tail#(cons(N, XS)) | → | U211#(isNatural(N), XS) |
| isNatural#(head(V1)) | → | isLNat#(V1) | | isLNat#(snd(V1)) | → | U81#(isPLNat(V1)) |
| tail#(cons(N, XS)) | → | isNatural#(N) | | U211#(tt, XS) | → | isLNat#(XS) |
| isLNat#(natsFrom(V1)) | → | isNatural#(V1) | | U211#(tt, XS) | → | U212#(isLNat(XS), XS) |
| U212#(tt, XS) | → | T(XS) | | head#(cons(N, XS)) | → | isNatural#(N) |
| U222#(tt, N, XS) | → | splitAt#(N, XS) | | U203#(tt, N, X, XS) | → | splitAt#(N, XS) |
| splitAt#(s(N), cons(X, XS)) | → | U201#(isNatural(N), N, X, XS) | | isNatural#(s(V1)) | → | U121#(isNatural(V1)) |
| U21#(tt, X, Y) | → | isLNat#(Y) | | isLNat#(fst(V1)) | → | U61#(isPLNat(V1)) |
| isLNat#(snd(V1)) | → | isPLNat#(V1) | | U12#(tt, N, XS) | → | snd#(splitAt(N, XS)) |
| isLNat#(tail(V1)) | → | isLNat#(V1) | | U181#(tt, Y) | → | isLNat#(Y) |
| U203#(tt, N, X, XS) | → | U204#(splitAt(N, XS), X) | | isLNat#(tail(V1)) | → | U91#(isLNat(V1)) |
| isLNat#(natsFrom(V1)) | → | U71#(isNatural(V1)) | | U172#(tt, N, XS) | → | afterNth#(N, XS) |
| isLNat#(fst(V1)) | → | isPLNat#(V1) | | isLNat#(cons(V1, V2)) | → | U51#(isNatural(V1), V2) |
| U11#(tt, N, XS) | → | U12#(isLNat(XS), N, XS) | | U202#(tt, N, X, XS) | → | U203#(isLNat(XS), N, X, XS) |
| snd#(pair(X, Y)) | → | U181#(isLNat(X), Y) | | U141#(tt, V2) | → | U142#(isLNat(V2)) |
| U31#(tt, N, XS) | → | isLNat#(XS) | | U12#(tt, N, XS) | → | splitAt#(N, XS) |
| U161#(tt, N) | → | T(N) | | U171#(tt, N, XS) | → | U172#(isLNat(XS), N, XS) |
| T(natsFrom(x_1)) | → | T(x_1) | | natsFrom#(N) | → | U161#(isNatural(N), N) |
| U12#(tt, N, XS) | → | T(XS) | | U172#(tt, N, XS) | → | head#(afterNth(N, XS)) |
| U151#(tt, V2) | → | U152#(isLNat(V2)) | | head#(cons(N, XS)) | → | U31#(isNatural(N), N, XS) |
| U12#(tt, N, XS) | → | T(N) | | U32#(tt, N) | → | T(N) |
| U151#(tt, V2) | → | isLNat#(V2) | | afterNth#(N, XS) | → | U11#(isNatural(N), N, XS) |
| U201#(tt, N, X, XS) | → | U202#(isNatural(X), N, X, XS) | | isNatural#(head(V1)) | → | U111#(isLNat(V1)) |
| isLNat#(take(V1, V2)) | → | U101#(isNatural(V1), V2) | | U203#(tt, N, X, XS) | → | T(N) |
| U191#(tt, XS) | → | T(XS) | | U222#(tt, N, XS) | → | fst#(splitAt(N, XS)) |
| U101#(tt, V2) | → | U102#(isLNat(V2)) | | U171#(tt, N, XS) | → | isLNat#(XS) |
| sel#(N, XS) | → | U171#(isNatural(N), N, XS) | | U222#(tt, N, XS) | → | T(XS) |
| U41#(tt, V2) | → | U42#(isLNat(V2)) | | isLNat#(cons(V1, V2)) | → | isNatural#(V1) |
| isLNat#(afterNth(V1, V2)) | → | isNatural#(V1) | | T(s(x_1)) | → | T(x_1) |
| U204#(pair(YS, ZS), X) | → | T(X) | | isNatural#(s(V1)) | → | isNatural#(V1) |
| isLNat#(afterNth(V1, V2)) | → | U41#(isNatural(V1), V2) | | isPLNat#(pair(V1, V2)) | → | U141#(isLNat(V1), V2) |
| U51#(tt, V2) | → | U52#(isLNat(V2)) | | isLNat#(take(V1, V2)) | → | isNatural#(V1) |
| snd#(pair(X, Y)) | → | isLNat#(X) | | splitAt#(0, XS) | → | isLNat#(XS) |
| natsFrom#(N) | → | isNatural#(N) | | U202#(tt, N, X, XS) | → | isLNat#(XS) |
| T(natsFrom(s(N))) | → | natsFrom#(s(N)) | | isNatural#(sel(V1, V2)) | → | U131#(isNatural(V1), V2) |
| U221#(tt, N, XS) | → | U222#(isLNat(XS), N, XS) | | isPLNat#(splitAt(V1, V2)) | → | U151#(isNatural(V1), V2) |
| U221#(tt, N, XS) | → | isLNat#(XS) | | fst#(pair(X, Y)) | → | isLNat#(X) |
| sel#(N, XS) | → | isNatural#(N) | | fst#(pair(X, Y)) | → | U21#(isLNat(X), X, Y) |
| isNatural#(sel(V1, V2)) | → | isNatural#(V1) | | U201#(tt, N, X, XS) | → | isNatural#(X) |
| take#(N, XS) | → | isNatural#(N) | | U31#(tt, N, XS) | → | U32#(isLNat(XS), N) |
| U131#(tt, V2) | → | U132#(isLNat(V2)) | | U141#(tt, V2) | → | isLNat#(V2) |
| U172#(tt, N, XS) | → | T(N) | | U101#(tt, V2) | → | isLNat#(V2) |
| afterNth#(N, XS) | → | isNatural#(N) | | U41#(tt, V2) | → | isLNat#(V2) |
| isPLNat#(pair(V1, V2)) | → | isLNat#(V1) | | U131#(tt, V2) | → | isLNat#(V2) |
| take#(N, XS) | → | U221#(isNatural(N), N, XS) | | splitAt#(0, XS) | → | U191#(isLNat(XS), XS) |
| U172#(tt, N, XS) | → | T(XS) | | U203#(tt, N, X, XS) | → | T(XS) |
| isPLNat#(splitAt(V1, V2)) | → | isNatural#(V1) | | U222#(tt, N, XS) | → | T(N) |
| U51#(tt, V2) | → | isLNat#(V2) | | U181#(tt, Y) | → | U182#(isLNat(Y), Y) |
Rewrite Rules
| U101(tt, V2) | → | U102(isLNat(V2)) | | U102(tt) | → | tt |
| U11(tt, N, XS) | → | U12(isLNat(XS), N, XS) | | U111(tt) | → | tt |
| U12(tt, N, XS) | → | snd(splitAt(N, XS)) | | U121(tt) | → | tt |
| U131(tt, V2) | → | U132(isLNat(V2)) | | U132(tt) | → | tt |
| U141(tt, V2) | → | U142(isLNat(V2)) | | U142(tt) | → | tt |
| U151(tt, V2) | → | U152(isLNat(V2)) | | U152(tt) | → | tt |
| U161(tt, N) | → | cons(N, natsFrom(s(N))) | | U171(tt, N, XS) | → | U172(isLNat(XS), N, XS) |
| U172(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | U182(isLNat(Y), Y) |
| U182(tt, Y) | → | Y | | U191(tt, XS) | → | pair(nil, XS) |
| U201(tt, N, X, XS) | → | U202(isNatural(X), N, X, XS) | | U202(tt, N, X, XS) | → | U203(isLNat(XS), N, X, XS) |
| U203(tt, N, X, XS) | → | U204(splitAt(N, XS), X) | | U204(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) |
| U21(tt, X, Y) | → | U22(isLNat(Y), X) | | U211(tt, XS) | → | U212(isLNat(XS), XS) |
| U212(tt, XS) | → | XS | | U22(tt, X) | → | X |
| U221(tt, N, XS) | → | U222(isLNat(XS), N, XS) | | U222(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N, XS) | → | U32(isLNat(XS), N) | | U32(tt, N) | → | N |
| U41(tt, V2) | → | U42(isLNat(V2)) | | U42(tt) | → | tt |
| U51(tt, V2) | → | U52(isLNat(V2)) | | U52(tt) | → | tt |
| U61(tt) | → | tt | | U71(tt) | → | tt |
| U81(tt) | → | tt | | U91(tt) | → | tt |
| afterNth(N, XS) | → | U11(isNatural(N), N, XS) | | fst(pair(X, Y)) | → | U21(isLNat(X), X, Y) |
| head(cons(N, XS)) | → | U31(isNatural(N), N, XS) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(isNatural(V1), V2) | | isLNat(cons(V1, V2)) | → | U51(isNatural(V1), V2) |
| isLNat(fst(V1)) | → | U61(isPLNat(V1)) | | isLNat(natsFrom(V1)) | → | U71(isNatural(V1)) |
| isLNat(snd(V1)) | → | U81(isPLNat(V1)) | | isLNat(tail(V1)) | → | U91(isLNat(V1)) |
| isLNat(take(V1, V2)) | → | U101(isNatural(V1), V2) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNat(V1)) | | isNatural(s(V1)) | → | U121(isNatural(V1)) |
| isNatural(sel(V1, V2)) | → | U131(isNatural(V1), V2) | | isPLNat(pair(V1, V2)) | → | U141(isLNat(V1), V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(isNatural(V1), V2) | | natsFrom(N) | → | U161(isNatural(N), N) |
| sel(N, XS) | → | U171(isNatural(N), N, XS) | | snd(pair(X, Y)) | → | U181(isLNat(X), Y) |
| splitAt(0, XS) | → | U191(isLNat(XS), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(isNatural(N), N, X, XS) |
| tail(cons(N, XS)) | → | U211(isNatural(N), XS) | | take(N, XS) | → | U221(isNatural(N), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U204, U203, fst, U111, U61, U211, U212, head, U21, U22, U151, U152, isPLNat, tail, U71, U191, 0, U121, U221, U222, isLNat, U31, U32, U181, U182, pair, isNatural, U132, U131, U42, U41, U91, cons, snd, U171, U172, splitAt, U201, U142, U202, U141, s, U51, tt, take, U81, U52, U11, U12, afterNth, U102, sel, nil, U101
Strategy
Context-sensitive strategy:
μ(isNatural#) = μ(isPLNat) = μ(0) = μ(isLNat#) = μ(T) = μ(tt) = μ(isLNat) = μ(isNatural) = μ(isPLNat#) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(fst#) = μ(U31#) = μ(U181#) = μ(U203#) = μ(tail#) = μ(U52#) = μ(U111) = μ(U61) = μ(U161#) = μ(U212#) = μ(U12#) = μ(U182#) = μ(U202#) = μ(U51#) = μ(tail) = μ(U71) = μ(U191) = μ(U71#) = μ(U121) = μ(U222#) = μ(U32#) = μ(U102#) = μ(U201#) = μ(U221#) = μ(U132) = μ(U131) = μ(U42) = μ(U41) = μ(U142#) = μ(cons) = μ(U101#) = μ(U121#) = μ(U142) = μ(U141) = μ(U51) = μ(s) = μ(U52) = μ(U141#) = μ(U151#) = μ(natsFrom) = μ(U21#) = μ(U161) = μ(U204) = μ(U203) = μ(U171#) = μ(fst) = μ(U41#) = μ(U211) = μ(U212) = μ(snd#) = μ(head) = μ(U21) = μ(U22) = μ(U152#) = μ(U22#) = μ(U61#) = μ(U151) = μ(U152) = μ(U172#) = μ(U42#) = μ(U191#) = μ(U221) = μ(U222) = μ(U31) = μ(U32) = μ(U181) = μ(U182) = μ(U91#) = μ(U81#) = μ(U211#) = μ(U91) = μ(U132#) = μ(U111#) = μ(snd) = μ(U171) = μ(U172) = μ(U201) = μ(U202) = μ(U204#) = μ(U81) = μ(U11) = μ(U12) = μ(U131#) = μ(head#) = μ(U102) = μ(U101) = {1}
μ(sel#) = μ(take#) = μ(pair) = μ(splitAt) = μ(afterNth) = μ(splitAt#) = μ(afterNth#) = μ(take) = μ(sel) = {1, 2}
The following SCCs where found
| isPLNat#(pair(V1, V2)) → isLNat#(V1) | U41#(tt, V2) → isLNat#(V2) |
| U131#(tt, V2) → isLNat#(V2) | isLNat#(snd(V1)) → isPLNat#(V1) |
| isLNat#(fst(V1)) → isPLNat#(V1) | isNatural#(head(V1)) → isLNat#(V1) |
| isNatural#(sel(V1, V2)) → isNatural#(V1) | isLNat#(cons(V1, V2)) → U51#(isNatural(V1), V2) |
| isLNat#(tail(V1)) → isLNat#(V1) | isNatural#(sel(V1, V2)) → U131#(isNatural(V1), V2) |
| isLNat#(natsFrom(V1)) → isNatural#(V1) | U151#(tt, V2) → isLNat#(V2) |
| isLNat#(cons(V1, V2)) → isNatural#(V1) | isLNat#(afterNth(V1, V2)) → isNatural#(V1) |
| isPLNat#(splitAt(V1, V2)) → U151#(isNatural(V1), V2) | isLNat#(take(V1, V2)) → U101#(isNatural(V1), V2) |
| U141#(tt, V2) → isLNat#(V2) | isNatural#(s(V1)) → isNatural#(V1) |
| U101#(tt, V2) → isLNat#(V2) | isLNat#(afterNth(V1, V2)) → U41#(isNatural(V1), V2) |
| isPLNat#(pair(V1, V2)) → U141#(isLNat(V1), V2) | isPLNat#(splitAt(V1, V2)) → isNatural#(V1) |
| U51#(tt, V2) → isLNat#(V2) | isLNat#(take(V1, V2)) → isNatural#(V1) |
| U201#(tt, N, X, XS) → U202#(isNatural(X), N, X, XS) | U203#(tt, N, X, XS) → splitAt#(N, XS) |
| splitAt#(s(N), cons(X, XS)) → U201#(isNatural(N), N, X, XS) | U202#(tt, N, X, XS) → U203#(isLNat(XS), N, X, XS) |
| T(natsFrom(x_1)) → T(x_1) | natsFrom#(N) → U161#(isNatural(N), N) |
| T(s(x_1)) → T(x_1) | T(natsFrom(s(N))) → natsFrom#(s(N)) |
| U161#(tt, N) → T(N) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isPLNat#(pair(V1, V2)) | → | isLNat#(V1) | | U41#(tt, V2) | → | isLNat#(V2) |
| U131#(tt, V2) | → | isLNat#(V2) | | isLNat#(snd(V1)) | → | isPLNat#(V1) |
| isLNat#(fst(V1)) | → | isPLNat#(V1) | | isNatural#(head(V1)) | → | isLNat#(V1) |
| isLNat#(cons(V1, V2)) | → | U51#(isNatural(V1), V2) | | isNatural#(sel(V1, V2)) | → | isNatural#(V1) |
| isLNat#(tail(V1)) | → | isLNat#(V1) | | isNatural#(sel(V1, V2)) | → | U131#(isNatural(V1), V2) |
| isLNat#(natsFrom(V1)) | → | isNatural#(V1) | | U151#(tt, V2) | → | isLNat#(V2) |
| isLNat#(cons(V1, V2)) | → | isNatural#(V1) | | isLNat#(afterNth(V1, V2)) | → | isNatural#(V1) |
| isPLNat#(splitAt(V1, V2)) | → | U151#(isNatural(V1), V2) | | isLNat#(take(V1, V2)) | → | U101#(isNatural(V1), V2) |
| U141#(tt, V2) | → | isLNat#(V2) | | U101#(tt, V2) | → | isLNat#(V2) |
| isNatural#(s(V1)) | → | isNatural#(V1) | | isLNat#(afterNth(V1, V2)) | → | U41#(isNatural(V1), V2) |
| isPLNat#(splitAt(V1, V2)) | → | isNatural#(V1) | | isPLNat#(pair(V1, V2)) | → | U141#(isLNat(V1), V2) |
| U51#(tt, V2) | → | isLNat#(V2) | | isLNat#(take(V1, V2)) | → | isNatural#(V1) |
Rewrite Rules
| U101(tt, V2) | → | U102(isLNat(V2)) | | U102(tt) | → | tt |
| U11(tt, N, XS) | → | U12(isLNat(XS), N, XS) | | U111(tt) | → | tt |
| U12(tt, N, XS) | → | snd(splitAt(N, XS)) | | U121(tt) | → | tt |
| U131(tt, V2) | → | U132(isLNat(V2)) | | U132(tt) | → | tt |
| U141(tt, V2) | → | U142(isLNat(V2)) | | U142(tt) | → | tt |
| U151(tt, V2) | → | U152(isLNat(V2)) | | U152(tt) | → | tt |
| U161(tt, N) | → | cons(N, natsFrom(s(N))) | | U171(tt, N, XS) | → | U172(isLNat(XS), N, XS) |
| U172(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | U182(isLNat(Y), Y) |
| U182(tt, Y) | → | Y | | U191(tt, XS) | → | pair(nil, XS) |
| U201(tt, N, X, XS) | → | U202(isNatural(X), N, X, XS) | | U202(tt, N, X, XS) | → | U203(isLNat(XS), N, X, XS) |
| U203(tt, N, X, XS) | → | U204(splitAt(N, XS), X) | | U204(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) |
| U21(tt, X, Y) | → | U22(isLNat(Y), X) | | U211(tt, XS) | → | U212(isLNat(XS), XS) |
| U212(tt, XS) | → | XS | | U22(tt, X) | → | X |
| U221(tt, N, XS) | → | U222(isLNat(XS), N, XS) | | U222(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N, XS) | → | U32(isLNat(XS), N) | | U32(tt, N) | → | N |
| U41(tt, V2) | → | U42(isLNat(V2)) | | U42(tt) | → | tt |
| U51(tt, V2) | → | U52(isLNat(V2)) | | U52(tt) | → | tt |
| U61(tt) | → | tt | | U71(tt) | → | tt |
| U81(tt) | → | tt | | U91(tt) | → | tt |
| afterNth(N, XS) | → | U11(isNatural(N), N, XS) | | fst(pair(X, Y)) | → | U21(isLNat(X), X, Y) |
| head(cons(N, XS)) | → | U31(isNatural(N), N, XS) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(isNatural(V1), V2) | | isLNat(cons(V1, V2)) | → | U51(isNatural(V1), V2) |
| isLNat(fst(V1)) | → | U61(isPLNat(V1)) | | isLNat(natsFrom(V1)) | → | U71(isNatural(V1)) |
| isLNat(snd(V1)) | → | U81(isPLNat(V1)) | | isLNat(tail(V1)) | → | U91(isLNat(V1)) |
| isLNat(take(V1, V2)) | → | U101(isNatural(V1), V2) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNat(V1)) | | isNatural(s(V1)) | → | U121(isNatural(V1)) |
| isNatural(sel(V1, V2)) | → | U131(isNatural(V1), V2) | | isPLNat(pair(V1, V2)) | → | U141(isLNat(V1), V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(isNatural(V1), V2) | | natsFrom(N) | → | U161(isNatural(N), N) |
| sel(N, XS) | → | U171(isNatural(N), N, XS) | | snd(pair(X, Y)) | → | U181(isLNat(X), Y) |
| splitAt(0, XS) | → | U191(isLNat(XS), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(isNatural(N), N, X, XS) |
| tail(cons(N, XS)) | → | U211(isNatural(N), XS) | | take(N, XS) | → | U221(isNatural(N), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U204, U203, fst, U111, U61, U211, U212, head, U21, U22, U151, U152, isPLNat, tail, U71, U191, 0, U121, U221, U222, isLNat, U31, U32, U181, U182, pair, isNatural, U132, U131, U42, U41, U91, cons, snd, U171, U172, splitAt, U201, U142, U202, U141, s, U51, tt, take, U81, U52, U11, U12, afterNth, U102, sel, nil, U101
Strategy
Context-sensitive strategy:
μ(isNatural#) = μ(isPLNat) = μ(0) = μ(isLNat#) = μ(T) = μ(tt) = μ(isLNat) = μ(isNatural) = μ(isPLNat#) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(U31#) = μ(fst#) = μ(U181#) = μ(U203#) = μ(U52#) = μ(tail#) = μ(U111) = μ(U161#) = μ(U61) = μ(U212#) = μ(U12#) = μ(U182#) = μ(U202#) = μ(U51#) = μ(tail) = μ(U71) = μ(U191) = μ(U71#) = μ(U121) = μ(U222#) = μ(U32#) = μ(U102#) = μ(U201#) = μ(U221#) = μ(U132) = μ(U131) = μ(U42) = μ(U41) = μ(U142#) = μ(cons) = μ(U121#) = μ(U101#) = μ(U142) = μ(U141) = μ(s) = μ(U51) = μ(U52) = μ(U141#) = μ(U151#) = μ(natsFrom) = μ(U21#) = μ(U161) = μ(U204) = μ(U203) = μ(U171#) = μ(fst) = μ(U41#) = μ(U211) = μ(U212) = μ(snd#) = μ(head) = μ(U21) = μ(U22) = μ(U152#) = μ(U22#) = μ(U61#) = μ(U151) = μ(U152) = μ(U172#) = μ(U42#) = μ(U191#) = μ(U221) = μ(U222) = μ(U31) = μ(U32) = μ(U181) = μ(U182) = μ(U91#) = μ(U81#) = μ(U211#) = μ(U91) = μ(U132#) = μ(U111#) = μ(snd) = μ(U171) = μ(U172) = μ(U201) = μ(U202) = μ(U204#) = μ(U81) = μ(U11) = μ(U12) = μ(head#) = μ(U131#) = μ(U102) = μ(U101) = {1}
μ(sel#) = μ(take#) = μ(pair) = μ(splitAt) = μ(afterNth) = μ(splitAt#) = μ(afterNth#) = μ(take) = μ(sel) = {1, 2}
Polynomial Interpretation
- 0: 2
- U101(x,y): 2y + 1
- U101#(x,y): 2y + 2
- U102(x): 1
- U11(x,y,z): 0
- U111(x): 0
- U12(x,y,z): 0
- U121(x): 0
- U131(x,y): 0
- U131#(x,y): 2y
- U132(x): 0
- U141(x,y): y + x
- U141#(x,y): 2y + 2x
- U142(x): 0
- U151(x,y): y + 2
- U151#(x,y): 2y + 2
- U152(x): x + 1
- U161(x,y): 0
- U171(x,y,z): 0
- U172(x,y,z): 0
- U181(x,y): 0
- U182(x,y): 0
- U191(x,y): 0
- U201(x1,x2,x3,x4): 0
- U202(x1,x2,x3,x4): 0
- U203(x1,x2,x3,x4): 0
- U204(x,y): 0
- U21(x,y,z): 0
- U211(x,y): 0
- U212(x,y): 0
- U22(x,y): 0
- U221(x,y,z): 0
- U222(x,y,z): 0
- U31(x,y,z): 0
- U32(x,y): 0
- U41(x,y): y
- U41#(x,y): 2y + 1
- U42(x): 0
- U51(x,y): y + 2
- U51#(x,y): 2y + 2
- U52(x): 0
- U61(x): 0
- U71(x): 0
- U81(x): 1
- U91(x): 2x
- afterNth(x,y): y + 2x + 1
- cons(x,y): y + x + 1
- fst(x): x + 1
- head(x): 2x
- isLNat(x): x + 1
- isLNat#(x): 2x
- isNatural(x): 0
- isNatural#(x): 2x + 2
- isPLNat(x): x + 2
- isPLNat#(x): 2x
- natsFrom(x): 2x + 1
- nil: 2
- pair(x,y): y + 2x + 1
- s(x): 2x
- sel(x,y): y + x
- snd(x): x + 1
- splitAt(x,y): y + x + 1
- tail(x): 2x + 1
- take(x,y): 2y + 2x + 1
- tt: 0
Standard Usable rules
| U141(tt, V2) | → | U142(isLNat(V2)) | | U41(tt, V2) | → | U42(isLNat(V2)) |
| U151(tt, V2) | → | U152(isLNat(V2)) | | isPLNat(pair(V1, V2)) | → | U141(isLNat(V1), V2) |
| isLNat(nil) | → | tt | | isLNat(natsFrom(V1)) | → | U71(isNatural(V1)) |
| isNatural(0) | → | tt | | isNatural(head(V1)) | → | U111(isLNat(V1)) |
| isLNat(afterNth(V1, V2)) | → | U41(isNatural(V1), V2) | | U81(tt) | → | tt |
| isLNat(snd(V1)) | → | U81(isPLNat(V1)) | | isLNat(tail(V1)) | → | U91(isLNat(V1)) |
| U152(tt) | → | tt | | U102(tt) | → | tt |
| U61(tt) | → | tt | | U121(tt) | → | tt |
| U71(tt) | → | tt | | isLNat(fst(V1)) | → | U61(isPLNat(V1)) |
| U111(tt) | → | tt | | U131(tt, V2) | → | U132(isLNat(V2)) |
| U132(tt) | → | tt | | U42(tt) | → | tt |
| isLNat(cons(V1, V2)) | → | U51(isNatural(V1), V2) | | U101(tt, V2) | → | U102(isLNat(V2)) |
| U142(tt) | → | tt | | isLNat(take(V1, V2)) | → | U101(isNatural(V1), V2) |
| U91(tt) | → | tt | | U51(tt, V2) | → | U52(isLNat(V2)) |
| isPLNat(splitAt(V1, V2)) | → | U151(isNatural(V1), V2) | | isNatural(s(V1)) | → | U121(isNatural(V1)) |
| U52(tt) | → | tt | | isNatural(sel(V1, V2)) | → | U131(isNatural(V1), V2) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isLNat#(fst(V1)) | → | isPLNat#(V1) | | isNatural#(head(V1)) | → | isLNat#(V1) |
| U101#(tt, V2) | → | isLNat#(V2) | | isLNat#(afterNth(V1, V2)) | → | U41#(isNatural(V1), V2) |
| U41#(tt, V2) | → | isLNat#(V2) | | isPLNat#(pair(V1, V2)) | → | isLNat#(V1) |
| isLNat#(snd(V1)) | → | isPLNat#(V1) | | isLNat#(tail(V1)) | → | isLNat#(V1) |
| isNatural#(sel(V1, V2)) | → | U131#(isNatural(V1), V2) | | U151#(tt, V2) | → | isLNat#(V2) |
| U51#(tt, V2) | → | isLNat#(V2) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U131#(tt, V2) | → | isLNat#(V2) | | isLNat#(cons(V1, V2)) | → | U51#(isNatural(V1), V2) |
| isNatural#(sel(V1, V2)) | → | isNatural#(V1) | | isLNat#(natsFrom(V1)) | → | isNatural#(V1) |
| isLNat#(cons(V1, V2)) | → | isNatural#(V1) | | isLNat#(afterNth(V1, V2)) | → | isNatural#(V1) |
| isPLNat#(splitAt(V1, V2)) | → | U151#(isNatural(V1), V2) | | isLNat#(take(V1, V2)) | → | U101#(isNatural(V1), V2) |
| U141#(tt, V2) | → | isLNat#(V2) | | isNatural#(s(V1)) | → | isNatural#(V1) |
| isPLNat#(splitAt(V1, V2)) | → | isNatural#(V1) | | isPLNat#(pair(V1, V2)) | → | U141#(isLNat(V1), V2) |
| isLNat#(take(V1, V2)) | → | isNatural#(V1) |
Rewrite Rules
| U101(tt, V2) | → | U102(isLNat(V2)) | | U102(tt) | → | tt |
| U11(tt, N, XS) | → | U12(isLNat(XS), N, XS) | | U111(tt) | → | tt |
| U12(tt, N, XS) | → | snd(splitAt(N, XS)) | | U121(tt) | → | tt |
| U131(tt, V2) | → | U132(isLNat(V2)) | | U132(tt) | → | tt |
| U141(tt, V2) | → | U142(isLNat(V2)) | | U142(tt) | → | tt |
| U151(tt, V2) | → | U152(isLNat(V2)) | | U152(tt) | → | tt |
| U161(tt, N) | → | cons(N, natsFrom(s(N))) | | U171(tt, N, XS) | → | U172(isLNat(XS), N, XS) |
| U172(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | U182(isLNat(Y), Y) |
| U182(tt, Y) | → | Y | | U191(tt, XS) | → | pair(nil, XS) |
| U201(tt, N, X, XS) | → | U202(isNatural(X), N, X, XS) | | U202(tt, N, X, XS) | → | U203(isLNat(XS), N, X, XS) |
| U203(tt, N, X, XS) | → | U204(splitAt(N, XS), X) | | U204(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) |
| U21(tt, X, Y) | → | U22(isLNat(Y), X) | | U211(tt, XS) | → | U212(isLNat(XS), XS) |
| U212(tt, XS) | → | XS | | U22(tt, X) | → | X |
| U221(tt, N, XS) | → | U222(isLNat(XS), N, XS) | | U222(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N, XS) | → | U32(isLNat(XS), N) | | U32(tt, N) | → | N |
| U41(tt, V2) | → | U42(isLNat(V2)) | | U42(tt) | → | tt |
| U51(tt, V2) | → | U52(isLNat(V2)) | | U52(tt) | → | tt |
| U61(tt) | → | tt | | U71(tt) | → | tt |
| U81(tt) | → | tt | | U91(tt) | → | tt |
| afterNth(N, XS) | → | U11(isNatural(N), N, XS) | | fst(pair(X, Y)) | → | U21(isLNat(X), X, Y) |
| head(cons(N, XS)) | → | U31(isNatural(N), N, XS) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(isNatural(V1), V2) | | isLNat(cons(V1, V2)) | → | U51(isNatural(V1), V2) |
| isLNat(fst(V1)) | → | U61(isPLNat(V1)) | | isLNat(natsFrom(V1)) | → | U71(isNatural(V1)) |
| isLNat(snd(V1)) | → | U81(isPLNat(V1)) | | isLNat(tail(V1)) | → | U91(isLNat(V1)) |
| isLNat(take(V1, V2)) | → | U101(isNatural(V1), V2) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNat(V1)) | | isNatural(s(V1)) | → | U121(isNatural(V1)) |
| isNatural(sel(V1, V2)) | → | U131(isNatural(V1), V2) | | isPLNat(pair(V1, V2)) | → | U141(isLNat(V1), V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(isNatural(V1), V2) | | natsFrom(N) | → | U161(isNatural(N), N) |
| sel(N, XS) | → | U171(isNatural(N), N, XS) | | snd(pair(X, Y)) | → | U181(isLNat(X), Y) |
| splitAt(0, XS) | → | U191(isLNat(XS), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(isNatural(N), N, X, XS) |
| tail(cons(N, XS)) | → | U211(isNatural(N), XS) | | take(N, XS) | → | U221(isNatural(N), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U204, U203, fst, U111, U61, U211, U212, head, U21, U22, U151, isPLNat, U152, tail, U191, U71, 0, U121, U221, isLNat, U222, U31, U32, U181, U182, pair, isNatural, U132, U131, U42, U41, U91, cons, snd, U171, U172, splitAt, U201, U142, U202, U141, s, U51, tt, take, U81, U52, U11, U12, afterNth, U102, sel, U101, nil
Strategy
Context-sensitive strategy:
μ(isNatural#) = μ(isPLNat) = μ(0) = μ(isLNat#) = μ(T) = μ(tt) = μ(isLNat) = μ(isNatural) = μ(isPLNat#) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(fst#) = μ(U31#) = μ(U181#) = μ(U203#) = μ(tail#) = μ(U52#) = μ(U111) = μ(U61) = μ(U161#) = μ(U212#) = μ(U12#) = μ(U182#) = μ(U202#) = μ(U51#) = μ(tail) = μ(U71) = μ(U191) = μ(U71#) = μ(U121) = μ(U222#) = μ(U32#) = μ(U102#) = μ(U201#) = μ(U221#) = μ(U132) = μ(U131) = μ(U42) = μ(U41) = μ(U142#) = μ(cons) = μ(U101#) = μ(U121#) = μ(U142) = μ(U141) = μ(U51) = μ(s) = μ(U52) = μ(U141#) = μ(U151#) = μ(natsFrom) = μ(U21#) = μ(U161) = μ(U204) = μ(U203) = μ(U171#) = μ(fst) = μ(U41#) = μ(U211) = μ(U212) = μ(snd#) = μ(head) = μ(U21) = μ(U22) = μ(U152#) = μ(U22#) = μ(U61#) = μ(U151) = μ(U152) = μ(U172#) = μ(U42#) = μ(U191#) = μ(U221) = μ(U222) = μ(U31) = μ(U32) = μ(U181) = μ(U182) = μ(U91#) = μ(U81#) = μ(U211#) = μ(U91) = μ(U132#) = μ(U111#) = μ(snd) = μ(U171) = μ(U172) = μ(U201) = μ(U202) = μ(U204#) = μ(U81) = μ(U11) = μ(U12) = μ(U131#) = μ(head#) = μ(U102) = μ(U101) = {1}
μ(sel#) = μ(take#) = μ(pair) = μ(splitAt) = μ(afterNth) = μ(splitAt#) = μ(afterNth#) = μ(take) = μ(sel) = {1, 2}
The following SCCs where found
| isNatural#(s(V1)) → isNatural#(V1) | isNatural#(sel(V1, V2)) → isNatural#(V1) |
Problem 6: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNatural#(s(V1)) | → | isNatural#(V1) | | isNatural#(sel(V1, V2)) | → | isNatural#(V1) |
Rewrite Rules
| U101(tt, V2) | → | U102(isLNat(V2)) | | U102(tt) | → | tt |
| U11(tt, N, XS) | → | U12(isLNat(XS), N, XS) | | U111(tt) | → | tt |
| U12(tt, N, XS) | → | snd(splitAt(N, XS)) | | U121(tt) | → | tt |
| U131(tt, V2) | → | U132(isLNat(V2)) | | U132(tt) | → | tt |
| U141(tt, V2) | → | U142(isLNat(V2)) | | U142(tt) | → | tt |
| U151(tt, V2) | → | U152(isLNat(V2)) | | U152(tt) | → | tt |
| U161(tt, N) | → | cons(N, natsFrom(s(N))) | | U171(tt, N, XS) | → | U172(isLNat(XS), N, XS) |
| U172(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | U182(isLNat(Y), Y) |
| U182(tt, Y) | → | Y | | U191(tt, XS) | → | pair(nil, XS) |
| U201(tt, N, X, XS) | → | U202(isNatural(X), N, X, XS) | | U202(tt, N, X, XS) | → | U203(isLNat(XS), N, X, XS) |
| U203(tt, N, X, XS) | → | U204(splitAt(N, XS), X) | | U204(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) |
| U21(tt, X, Y) | → | U22(isLNat(Y), X) | | U211(tt, XS) | → | U212(isLNat(XS), XS) |
| U212(tt, XS) | → | XS | | U22(tt, X) | → | X |
| U221(tt, N, XS) | → | U222(isLNat(XS), N, XS) | | U222(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N, XS) | → | U32(isLNat(XS), N) | | U32(tt, N) | → | N |
| U41(tt, V2) | → | U42(isLNat(V2)) | | U42(tt) | → | tt |
| U51(tt, V2) | → | U52(isLNat(V2)) | | U52(tt) | → | tt |
| U61(tt) | → | tt | | U71(tt) | → | tt |
| U81(tt) | → | tt | | U91(tt) | → | tt |
| afterNth(N, XS) | → | U11(isNatural(N), N, XS) | | fst(pair(X, Y)) | → | U21(isLNat(X), X, Y) |
| head(cons(N, XS)) | → | U31(isNatural(N), N, XS) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(isNatural(V1), V2) | | isLNat(cons(V1, V2)) | → | U51(isNatural(V1), V2) |
| isLNat(fst(V1)) | → | U61(isPLNat(V1)) | | isLNat(natsFrom(V1)) | → | U71(isNatural(V1)) |
| isLNat(snd(V1)) | → | U81(isPLNat(V1)) | | isLNat(tail(V1)) | → | U91(isLNat(V1)) |
| isLNat(take(V1, V2)) | → | U101(isNatural(V1), V2) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNat(V1)) | | isNatural(s(V1)) | → | U121(isNatural(V1)) |
| isNatural(sel(V1, V2)) | → | U131(isNatural(V1), V2) | | isPLNat(pair(V1, V2)) | → | U141(isLNat(V1), V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(isNatural(V1), V2) | | natsFrom(N) | → | U161(isNatural(N), N) |
| sel(N, XS) | → | U171(isNatural(N), N, XS) | | snd(pair(X, Y)) | → | U181(isLNat(X), Y) |
| splitAt(0, XS) | → | U191(isLNat(XS), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(isNatural(N), N, X, XS) |
| tail(cons(N, XS)) | → | U211(isNatural(N), XS) | | take(N, XS) | → | U221(isNatural(N), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U204, U203, fst, U111, U61, U211, U212, head, U21, U22, U151, isPLNat, U152, tail, U191, U71, 0, U121, U221, isLNat, U222, U31, U32, U181, U182, pair, isNatural, U132, U131, U42, U41, U91, cons, snd, U171, U172, splitAt, U201, U142, U202, U141, s, U51, tt, take, U81, U52, U11, U12, afterNth, U102, sel, U101, nil
Strategy
Context-sensitive strategy:
μ(isNatural#) = μ(isPLNat) = μ(0) = μ(isLNat#) = μ(T) = μ(tt) = μ(isLNat) = μ(isNatural) = μ(isPLNat#) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(U31#) = μ(fst#) = μ(U181#) = μ(U203#) = μ(U52#) = μ(tail#) = μ(U111) = μ(U161#) = μ(U61) = μ(U212#) = μ(U12#) = μ(U182#) = μ(U202#) = μ(U51#) = μ(tail) = μ(U71) = μ(U191) = μ(U71#) = μ(U121) = μ(U222#) = μ(U32#) = μ(U102#) = μ(U201#) = μ(U221#) = μ(U132) = μ(U131) = μ(U42) = μ(U41) = μ(U142#) = μ(cons) = μ(U121#) = μ(U101#) = μ(U142) = μ(U141) = μ(s) = μ(U51) = μ(U52) = μ(U141#) = μ(U151#) = μ(natsFrom) = μ(U21#) = μ(U161) = μ(U204) = μ(U203) = μ(U171#) = μ(fst) = μ(U41#) = μ(U211) = μ(U212) = μ(snd#) = μ(head) = μ(U21) = μ(U22) = μ(U152#) = μ(U22#) = μ(U61#) = μ(U151) = μ(U152) = μ(U172#) = μ(U42#) = μ(U191#) = μ(U221) = μ(U222) = μ(U31) = μ(U32) = μ(U181) = μ(U182) = μ(U91#) = μ(U81#) = μ(U211#) = μ(U91) = μ(U132#) = μ(U111#) = μ(snd) = μ(U171) = μ(U172) = μ(U201) = μ(U202) = μ(U204#) = μ(U81) = μ(U11) = μ(U12) = μ(head#) = μ(U131#) = μ(U102) = μ(U101) = {1}
μ(sel#) = μ(take#) = μ(pair) = μ(splitAt) = μ(afterNth) = μ(splitAt#) = μ(afterNth#) = μ(take) = μ(sel) = {1, 2}
Polynomial Interpretation
- 0: 0
- U101(x,y): 0
- U102(x): 0
- U11(x,y,z): 0
- U111(x): 0
- U12(x,y,z): 0
- U121(x): 0
- U131(x,y): 0
- U132(x): 0
- U141(x,y): 0
- U142(x): 0
- U151(x,y): 0
- U152(x): 0
- U161(x,y): 0
- U171(x,y,z): 0
- U172(x,y,z): 0
- U181(x,y): 0
- U182(x,y): 0
- U191(x,y): 0
- U201(x1,x2,x3,x4): 0
- U202(x1,x2,x3,x4): 0
- U203(x1,x2,x3,x4): 0
- U204(x,y): 0
- U21(x,y,z): 0
- U211(x,y): 0
- U212(x,y): 0
- U22(x,y): 0
- U221(x,y,z): 0
- U222(x,y,z): 0
- U31(x,y,z): 0
- U32(x,y): 0
- U41(x,y): 0
- U42(x): 0
- U51(x,y): 0
- U52(x): 0
- U61(x): 0
- U71(x): 0
- U81(x): 0
- U91(x): 0
- afterNth(x,y): 0
- cons(x,y): 0
- fst(x): 0
- head(x): 0
- isLNat(x): 0
- isNatural(x): 0
- isNatural#(x): 2x
- isPLNat(x): 0
- natsFrom(x): 0
- nil: 0
- pair(x,y): 0
- s(x): x + 1
- sel(x,y): x
- snd(x): 0
- splitAt(x,y): 0
- tail(x): 0
- take(x,y): 0
- 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:
| isNatural#(s(V1)) | → | isNatural#(V1) |
Problem 7: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNatural#(sel(V1, V2)) | → | isNatural#(V1) |
Rewrite Rules
| U101(tt, V2) | → | U102(isLNat(V2)) | | U102(tt) | → | tt |
| U11(tt, N, XS) | → | U12(isLNat(XS), N, XS) | | U111(tt) | → | tt |
| U12(tt, N, XS) | → | snd(splitAt(N, XS)) | | U121(tt) | → | tt |
| U131(tt, V2) | → | U132(isLNat(V2)) | | U132(tt) | → | tt |
| U141(tt, V2) | → | U142(isLNat(V2)) | | U142(tt) | → | tt |
| U151(tt, V2) | → | U152(isLNat(V2)) | | U152(tt) | → | tt |
| U161(tt, N) | → | cons(N, natsFrom(s(N))) | | U171(tt, N, XS) | → | U172(isLNat(XS), N, XS) |
| U172(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | U182(isLNat(Y), Y) |
| U182(tt, Y) | → | Y | | U191(tt, XS) | → | pair(nil, XS) |
| U201(tt, N, X, XS) | → | U202(isNatural(X), N, X, XS) | | U202(tt, N, X, XS) | → | U203(isLNat(XS), N, X, XS) |
| U203(tt, N, X, XS) | → | U204(splitAt(N, XS), X) | | U204(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) |
| U21(tt, X, Y) | → | U22(isLNat(Y), X) | | U211(tt, XS) | → | U212(isLNat(XS), XS) |
| U212(tt, XS) | → | XS | | U22(tt, X) | → | X |
| U221(tt, N, XS) | → | U222(isLNat(XS), N, XS) | | U222(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N, XS) | → | U32(isLNat(XS), N) | | U32(tt, N) | → | N |
| U41(tt, V2) | → | U42(isLNat(V2)) | | U42(tt) | → | tt |
| U51(tt, V2) | → | U52(isLNat(V2)) | | U52(tt) | → | tt |
| U61(tt) | → | tt | | U71(tt) | → | tt |
| U81(tt) | → | tt | | U91(tt) | → | tt |
| afterNth(N, XS) | → | U11(isNatural(N), N, XS) | | fst(pair(X, Y)) | → | U21(isLNat(X), X, Y) |
| head(cons(N, XS)) | → | U31(isNatural(N), N, XS) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(isNatural(V1), V2) | | isLNat(cons(V1, V2)) | → | U51(isNatural(V1), V2) |
| isLNat(fst(V1)) | → | U61(isPLNat(V1)) | | isLNat(natsFrom(V1)) | → | U71(isNatural(V1)) |
| isLNat(snd(V1)) | → | U81(isPLNat(V1)) | | isLNat(tail(V1)) | → | U91(isLNat(V1)) |
| isLNat(take(V1, V2)) | → | U101(isNatural(V1), V2) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNat(V1)) | | isNatural(s(V1)) | → | U121(isNatural(V1)) |
| isNatural(sel(V1, V2)) | → | U131(isNatural(V1), V2) | | isPLNat(pair(V1, V2)) | → | U141(isLNat(V1), V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(isNatural(V1), V2) | | natsFrom(N) | → | U161(isNatural(N), N) |
| sel(N, XS) | → | U171(isNatural(N), N, XS) | | snd(pair(X, Y)) | → | U181(isLNat(X), Y) |
| splitAt(0, XS) | → | U191(isLNat(XS), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(isNatural(N), N, X, XS) |
| tail(cons(N, XS)) | → | U211(isNatural(N), XS) | | take(N, XS) | → | U221(isNatural(N), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U204, U203, fst, U111, U61, U211, U212, head, U21, U22, U151, U152, isPLNat, tail, U71, U191, 0, U121, U221, U222, isLNat, U31, U32, U181, U182, pair, isNatural, U132, U131, U42, U41, U91, cons, snd, U171, U172, splitAt, U201, U142, U202, U141, s, U51, tt, take, U81, U52, U11, U12, afterNth, U102, sel, nil, U101
Strategy
Context-sensitive strategy:
μ(isNatural#) = μ(isPLNat) = μ(0) = μ(isLNat#) = μ(T) = μ(tt) = μ(isLNat) = μ(isNatural) = μ(isPLNat#) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(fst#) = μ(U31#) = μ(U181#) = μ(U203#) = μ(tail#) = μ(U52#) = μ(U111) = μ(U61) = μ(U161#) = μ(U212#) = μ(U12#) = μ(U182#) = μ(U202#) = μ(U51#) = μ(tail) = μ(U71) = μ(U191) = μ(U71#) = μ(U121) = μ(U222#) = μ(U32#) = μ(U102#) = μ(U201#) = μ(U221#) = μ(U132) = μ(U131) = μ(U42) = μ(U41) = μ(U142#) = μ(cons) = μ(U101#) = μ(U121#) = μ(U142) = μ(U141) = μ(U51) = μ(s) = μ(U52) = μ(U141#) = μ(U151#) = μ(natsFrom) = μ(U21#) = μ(U161) = μ(U204) = μ(U203) = μ(U171#) = μ(fst) = μ(U41#) = μ(U211) = μ(U212) = μ(snd#) = μ(head) = μ(U21) = μ(U22) = μ(U152#) = μ(U22#) = μ(U61#) = μ(U151) = μ(U152) = μ(U172#) = μ(U42#) = μ(U191#) = μ(U221) = μ(U222) = μ(U31) = μ(U32) = μ(U181) = μ(U182) = μ(U91#) = μ(U81#) = μ(U211#) = μ(U91) = μ(U132#) = μ(U111#) = μ(snd) = μ(U171) = μ(U172) = μ(U201) = μ(U202) = μ(U204#) = μ(U81) = μ(U11) = μ(U12) = μ(U131#) = μ(head#) = μ(U102) = μ(U101) = {1}
μ(sel#) = μ(take#) = μ(pair) = μ(splitAt) = μ(afterNth) = μ(splitAt#) = μ(afterNth#) = μ(take) = μ(sel) = {1, 2}
Polynomial Interpretation
- 0: 0
- U101(x,y): 0
- U102(x): 0
- U11(x,y,z): 0
- U111(x): 0
- U12(x,y,z): 0
- U121(x): 0
- U131(x,y): 0
- U132(x): 0
- U141(x,y): 0
- U142(x): 0
- U151(x,y): 0
- U152(x): 0
- U161(x,y): 0
- U171(x,y,z): 0
- U172(x,y,z): 0
- U181(x,y): 0
- U182(x,y): 0
- U191(x,y): 0
- U201(x1,x2,x3,x4): 0
- U202(x1,x2,x3,x4): 0
- U203(x1,x2,x3,x4): 0
- U204(x,y): 0
- U21(x,y,z): 0
- U211(x,y): 0
- U212(x,y): 0
- U22(x,y): 0
- U221(x,y,z): 0
- U222(x,y,z): 0
- U31(x,y,z): 0
- U32(x,y): 0
- U41(x,y): 0
- U42(x): 0
- U51(x,y): 0
- U52(x): 0
- U61(x): 0
- U71(x): 0
- U81(x): 0
- U91(x): 0
- afterNth(x,y): 0
- cons(x,y): 0
- fst(x): 0
- head(x): 0
- isLNat(x): 0
- isNatural(x): 0
- isNatural#(x): x + 1
- isPLNat(x): 0
- natsFrom(x): 0
- nil: 0
- pair(x,y): 0
- s(x): 0
- sel(x,y): x + 1
- snd(x): 0
- splitAt(x,y): 0
- tail(x): 0
- take(x,y): 0
- 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:
| isNatural#(sel(V1, V2)) | → | isNatural#(V1) |