TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60001 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (5882ms).
| – Problem 2 was processed with processor DependencyGraph (14ms).
| – Problem 3 was processed with processor DependencyGraph (30ms).
| – Problem 4 was processed with processor DependencyGraph (10ms).
| – Problem 5 was processed with processor DependencyGraph (4ms).
| – Problem 6 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (1ms), SubtermCriterion (0ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (1ms), DependencyGraph (1ms), PolynomialOrderingProcessor (0ms), DependencyGraph (1ms), PolynomialLinearRange4 (1124ms), DependencyGraph (2ms), ReductionPairSAT (3495ms), DependencyGraph (1ms), SizeChangePrinciple (timeout)].
| – Problem 7 was processed with processor DependencyGraph (12ms).
| – Problem 8 was processed with processor DependencyGraph (1ms).
| – Problem 9 was processed with processor DependencyGraph (12ms).
| – Problem 10 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (1470ms), SubtermCriterion (0ms), DependencyGraph (1453ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (1458ms), PolynomialOrderingProcessor (0ms), DependencyGraph (1455ms), PolynomialLinearRange4 (2618ms), DependencyGraph (1467ms), ReductionPairSAT (6410ms), DependencyGraph (1456ms)].
| – Problem 11 was processed with processor DependencyGraph (1ms).
The following open problems remain:
Open Dependency Pair Problem 6
Dependency Pairs
| splitAt#(s(N), cons(X, XS)) | → | U201#(and(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) | | U201#(tt, N, X, XS) | → | splitAt#(N, XS) |
Rewrite Rules
| U101(tt, V1, V2) | → | U102(isNatural(V1), V2) | | U102(tt, V2) | → | U103(isLNat(V2)) |
| U103(tt) | → | tt | | U11(tt, N, XS) | → | snd(splitAt(N, XS)) |
| U111(tt, V1) | → | U112(isLNat(V1)) | | U112(tt) | → | tt |
| U121(tt, V1) | → | U122(isNatural(V1)) | | U122(tt) | → | tt |
| U131(tt, V1, V2) | → | U132(isNatural(V1), V2) | | U132(tt, V2) | → | U133(isLNat(V2)) |
| U133(tt) | → | tt | | U141(tt, V1, V2) | → | U142(isLNat(V1), V2) |
| U142(tt, V2) | → | U143(isLNat(V2)) | | U143(tt) | → | tt |
| U151(tt, V1, V2) | → | U152(isNatural(V1), V2) | | U152(tt, V2) | → | U153(isLNat(V2)) |
| U153(tt) | → | tt | | U161(tt, N) | → | cons(N, natsFrom(s(N))) |
| U171(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | Y |
| U191(tt, XS) | → | pair(nil, XS) | | U201(tt, N, X, XS) | → | U202(splitAt(N, XS), X) |
| U202(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) | | U21(tt, X) | → | X |
| U211(tt, XS) | → | XS | | U221(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N) | → | N | | U41(tt, V1, V2) | → | U42(isNatural(V1), V2) |
| U42(tt, V2) | → | U43(isLNat(V2)) | | U43(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNatural(V1), V2) | | U52(tt, V2) | → | U53(isLNat(V2)) |
| U53(tt) | → | tt | | U61(tt, V1) | → | U62(isPLNat(V1)) |
| U62(tt) | → | tt | | U71(tt, V1) | → | U72(isNatural(V1)) |
| U72(tt) | → | tt | | U81(tt, V1) | → | U82(isPLNat(V1)) |
| U82(tt) | → | tt | | U91(tt, V1) | → | U92(isLNat(V1)) |
| U92(tt) | → | tt | | afterNth(N, XS) | → | U11(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
| and(tt, X) | → | X | | fst(pair(X, Y)) | → | U21(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) |
| head(cons(N, XS)) | → | U31(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNat(cons(V1, V2)) | → | U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| isLNat(fst(V1)) | → | U61(isPLNatKind(V1), V1) | | isLNat(natsFrom(V1)) | → | U71(isNaturalKind(V1), V1) |
| isLNat(snd(V1)) | → | U81(isPLNatKind(V1), V1) | | isLNat(tail(V1)) | → | U91(isLNatKind(V1), V1) |
| isLNat(take(V1, V2)) | → | U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNatKind(nil) | → | tt |
| isLNatKind(afterNth(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isLNatKind(cons(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) |
| isLNatKind(fst(V1)) | → | isPLNatKind(V1) | | isLNatKind(natsFrom(V1)) | → | isNaturalKind(V1) |
| isLNatKind(snd(V1)) | → | isPLNatKind(V1) | | isLNatKind(tail(V1)) | → | isLNatKind(V1) |
| isLNatKind(take(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNatKind(V1), V1) | | isNatural(s(V1)) | → | U121(isNaturalKind(V1), V1) |
| isNatural(sel(V1, V2)) | → | U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isNaturalKind(0) | → | tt |
| isNaturalKind(head(V1)) | → | isLNatKind(V1) | | isNaturalKind(s(V1)) | → | isNaturalKind(V1) |
| isNaturalKind(sel(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isPLNat(pair(V1, V2)) | → | U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isPLNatKind(pair(V1, V2)) | → | and(isLNatKind(V1), isLNatKind(V2)) |
| isPLNatKind(splitAt(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | natsFrom(N) | → | U161(and(isNatural(N), isNaturalKind(N)), N) |
| sel(N, XS) | → | U171(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | | snd(pair(X, Y)) | → | U181(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) |
| splitAt(0, XS) | → | U191(and(isLNat(XS), isLNatKind(XS)), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(and(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) |
| tail(cons(N, XS)) | → | U211(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), XS) | | take(N, XS) | → | U221(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U112, fst, U111, U62, U61, U211, head, U21, U153, U151, isLNatKind, U152, isPLNat, tail, and, U71, U191, U72, 0, isPLNatKind, U122, U121, U221, isLNat, U31, U181, pair, isNatural, U132, U131, U43, U42, U92, U133, U41, U91, snd, cons, isNaturalKind, U171, splitAt, U143, U201, U142, U202, U141, s, U51, tt, take, U82, U53, U81, U52, U11, afterNth, U102, sel, U103, U101, nil
Open Dependency Pair Problem 10
Dependency Pairs
| isNaturalKind#(sel(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) | | T(isNaturalKind(X)) | → | isNaturalKind#(X) |
| T(and(x_1, x_2)) | → | T(x_1) | | isPLNat#(splitAt(V1, V2)) | → | isNaturalKind#(V1) |
| T(isNatural(X)) | → | isNatural#(X) | | U131#(tt, V1, V2) | → | isNatural#(V1) |
| isLNat#(snd(V1)) | → | isPLNatKind#(V1) | | isLNat#(take(V1, V2)) | → | U101#(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| U71#(tt, V1) | → | isNatural#(V1) | | U141#(tt, V1, V2) | → | isLNat#(V1) |
| U52#(tt, V2) | → | isLNat#(V2) | | U142#(tt, V2) | → | isLNat#(V2) |
| isNaturalKind#(sel(V1, V2)) | → | isNaturalKind#(V1) | | and#(tt, X) | → | T(X) |
| T(isLNatKind(Y)) | → | isLNatKind#(Y) | | U101#(tt, V1, V2) | → | U102#(isNatural(V1), V2) |
| isLNat#(afterNth(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) | | isPLNat#(pair(V1, V2)) | → | and#(isLNatKind(V1), isLNatKind(V2)) |
| U111#(tt, V1) | → | isLNat#(V1) | | U51#(tt, V1, V2) | → | isNatural#(V1) |
| U121#(tt, V1) | → | isNatural#(V1) | | isPLNatKind#(pair(V1, V2)) | → | isLNatKind#(V1) |
| T(isNaturalKind(N)) | → | isNaturalKind#(N) | | isLNat#(natsFrom(V1)) | → | U71#(isNaturalKind(V1), V1) |
| U61#(tt, V1) | → | isPLNat#(V1) | | T(isNatural(x_1)) | → | T(x_1) |
| isLNat#(cons(V1, V2)) | → | isNaturalKind#(V1) | | isLNatKind#(cons(V1, V2)) | → | isNaturalKind#(V1) |
| T(and(x_1, x_2)) | → | T(x_2) | | T(isLNatKind(XS)) | → | isLNatKind#(XS) |
| isPLNat#(pair(V1, V2)) | → | isLNatKind#(V1) | | isNatural#(s(V1)) | → | U121#(isNaturalKind(V1), V1) |
| isLNat#(tail(V1)) | → | isLNatKind#(V1) | | U152#(tt, V2) | → | isLNat#(V2) |
| isLNat#(cons(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) | | U161#(tt, N) | → | T(N) |
| U151#(tt, V1, V2) | → | isNatural#(V1) | | isPLNatKind#(splitAt(V1, V2)) | → | isNaturalKind#(V1) |
| U51#(tt, V1, V2) | → | U52#(isNatural(V1), V2) | | isNatural#(head(V1)) | → | isLNatKind#(V1) |
| T(natsFrom(x_1)) | → | T(x_1) | | isPLNat#(splitAt(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) |
| isNaturalKind#(s(V1)) | → | isNaturalKind#(V1) | | U81#(tt, V1) | → | isPLNat#(V1) |
| U41#(tt, V1, V2) | → | isNatural#(V1) | | isLNatKind#(take(V1, V2)) | → | isNaturalKind#(V1) |
| isLNat#(snd(V1)) | → | U81#(isPLNatKind(V1), V1) | | isPLNat#(pair(V1, V2)) | → | U141#(and(isLNatKind(V1), isLNatKind(V2)), V1, V2) |
| T(and(isLNat(Y), isLNatKind(Y))) | → | and#(isLNat(Y), isLNatKind(Y)) | | U102#(tt, V2) | → | isLNat#(V2) |
| isLNatKind#(cons(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) | | isLNat#(take(V1, V2)) | → | isNaturalKind#(V1) |
| T(isLNat(XS)) | → | isLNat#(XS) | | U141#(tt, V1, V2) | → | U142#(isLNat(V1), V2) |
| isLNatKind#(take(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) | | isPLNatKind#(pair(V1, V2)) | → | and#(isLNatKind(V1), isLNatKind(V2)) |
| T(and(isNatural(X), isNaturalKind(X))) | → | and#(isNatural(X), isNaturalKind(X)) | | isLNat#(natsFrom(V1)) | → | isNaturalKind#(V1) |
| T(and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))) | → | and#(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS))) | | T(s(x_1)) | → | T(x_1) |
| isNatural#(sel(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) | | isNatural#(sel(V1, V2)) | → | U131#(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| T(isLNatKind(V2)) | → | isLNatKind#(V2) | | isLNat#(afterNth(V1, V2)) | → | isNaturalKind#(V1) |
| natsFrom#(N) | → | isNatural#(N) | | isLNatKind#(snd(V1)) | → | isPLNatKind#(V1) |
| T(natsFrom(s(N))) | → | natsFrom#(s(N)) | | isLNatKind#(fst(V1)) | → | isPLNatKind#(V1) |
| isLNatKind#(afterNth(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) | | isNatural#(head(V1)) | → | U111#(isLNatKind(V1), V1) |
| U41#(tt, V1, V2) | → | U42#(isNatural(V1), V2) | | T(and(isLNat(XS), isLNatKind(XS))) | → | and#(isLNat(XS), isLNatKind(XS)) |
| natsFrom#(N) | → | U161#(and(isNatural(N), isNaturalKind(N)), N) | | isNaturalKind#(head(V1)) | → | isLNatKind#(V1) |
| U91#(tt, V1) | → | isLNat#(V1) | | isLNat#(tail(V1)) | → | U91#(isLNatKind(V1), V1) |
| T(isLNatKind(X)) | → | isLNatKind#(X) | | T(isLNat(Y)) | → | isLNat#(Y) |
| isLNat#(take(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) | | U151#(tt, V1, V2) | → | U152#(isNatural(V1), V2) |
| isPLNatKind#(splitAt(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) | | isNatural#(sel(V1, V2)) | → | isNaturalKind#(V1) |
| isNatural#(s(V1)) | → | isNaturalKind#(V1) | | isLNat#(fst(V1)) | → | U61#(isPLNatKind(V1), V1) |
| U132#(tt, V2) | → | isLNat#(V2) | | isLNatKind#(natsFrom(V1)) | → | isNaturalKind#(V1) |
| isLNat#(afterNth(V1, V2)) | → | U41#(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | T(isLNat(x_1)) | → | T(x_1) |
| isLNatKind#(tail(V1)) | → | isLNatKind#(V1) | | U131#(tt, V1, V2) | → | U132#(isNatural(V1), V2) |
| T(isLNatKind(x_1)) | → | T(x_1) | | isLNatKind#(afterNth(V1, V2)) | → | isNaturalKind#(V1) |
| isLNat#(cons(V1, V2)) | → | U51#(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNat#(fst(V1)) | → | isPLNatKind#(V1) |
| T(isNaturalKind(x_1)) | → | T(x_1) | | isPLNat#(splitAt(V1, V2)) | → | U151#(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| U101#(tt, V1, V2) | → | isNatural#(V1) | | natsFrom#(N) | → | and#(isNatural(N), isNaturalKind(N)) |
| U42#(tt, V2) | → | isLNat#(V2) |
Rewrite Rules
| U101(tt, V1, V2) | → | U102(isNatural(V1), V2) | | U102(tt, V2) | → | U103(isLNat(V2)) |
| U103(tt) | → | tt | | U11(tt, N, XS) | → | snd(splitAt(N, XS)) |
| U111(tt, V1) | → | U112(isLNat(V1)) | | U112(tt) | → | tt |
| U121(tt, V1) | → | U122(isNatural(V1)) | | U122(tt) | → | tt |
| U131(tt, V1, V2) | → | U132(isNatural(V1), V2) | | U132(tt, V2) | → | U133(isLNat(V2)) |
| U133(tt) | → | tt | | U141(tt, V1, V2) | → | U142(isLNat(V1), V2) |
| U142(tt, V2) | → | U143(isLNat(V2)) | | U143(tt) | → | tt |
| U151(tt, V1, V2) | → | U152(isNatural(V1), V2) | | U152(tt, V2) | → | U153(isLNat(V2)) |
| U153(tt) | → | tt | | U161(tt, N) | → | cons(N, natsFrom(s(N))) |
| U171(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | Y |
| U191(tt, XS) | → | pair(nil, XS) | | U201(tt, N, X, XS) | → | U202(splitAt(N, XS), X) |
| U202(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) | | U21(tt, X) | → | X |
| U211(tt, XS) | → | XS | | U221(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N) | → | N | | U41(tt, V1, V2) | → | U42(isNatural(V1), V2) |
| U42(tt, V2) | → | U43(isLNat(V2)) | | U43(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNatural(V1), V2) | | U52(tt, V2) | → | U53(isLNat(V2)) |
| U53(tt) | → | tt | | U61(tt, V1) | → | U62(isPLNat(V1)) |
| U62(tt) | → | tt | | U71(tt, V1) | → | U72(isNatural(V1)) |
| U72(tt) | → | tt | | U81(tt, V1) | → | U82(isPLNat(V1)) |
| U82(tt) | → | tt | | U91(tt, V1) | → | U92(isLNat(V1)) |
| U92(tt) | → | tt | | afterNth(N, XS) | → | U11(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
| and(tt, X) | → | X | | fst(pair(X, Y)) | → | U21(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) |
| head(cons(N, XS)) | → | U31(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNat(cons(V1, V2)) | → | U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| isLNat(fst(V1)) | → | U61(isPLNatKind(V1), V1) | | isLNat(natsFrom(V1)) | → | U71(isNaturalKind(V1), V1) |
| isLNat(snd(V1)) | → | U81(isPLNatKind(V1), V1) | | isLNat(tail(V1)) | → | U91(isLNatKind(V1), V1) |
| isLNat(take(V1, V2)) | → | U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNatKind(nil) | → | tt |
| isLNatKind(afterNth(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isLNatKind(cons(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) |
| isLNatKind(fst(V1)) | → | isPLNatKind(V1) | | isLNatKind(natsFrom(V1)) | → | isNaturalKind(V1) |
| isLNatKind(snd(V1)) | → | isPLNatKind(V1) | | isLNatKind(tail(V1)) | → | isLNatKind(V1) |
| isLNatKind(take(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNatKind(V1), V1) | | isNatural(s(V1)) | → | U121(isNaturalKind(V1), V1) |
| isNatural(sel(V1, V2)) | → | U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isNaturalKind(0) | → | tt |
| isNaturalKind(head(V1)) | → | isLNatKind(V1) | | isNaturalKind(s(V1)) | → | isNaturalKind(V1) |
| isNaturalKind(sel(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isPLNat(pair(V1, V2)) | → | U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isPLNatKind(pair(V1, V2)) | → | and(isLNatKind(V1), isLNatKind(V2)) |
| isPLNatKind(splitAt(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | natsFrom(N) | → | U161(and(isNatural(N), isNaturalKind(N)), N) |
| sel(N, XS) | → | U171(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | | snd(pair(X, Y)) | → | U181(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) |
| splitAt(0, XS) | → | U191(and(isLNat(XS), isLNatKind(XS)), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(and(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) |
| tail(cons(N, XS)) | → | U211(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), XS) | | take(N, XS) | → | U221(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U112, fst, U111, U62, U61, U211, head, U21, U153, U151, isLNatKind, U152, isPLNat, tail, and, U71, U191, U72, 0, isPLNatKind, U122, U121, U221, isLNat, U31, U181, pair, isNatural, U132, U131, U43, U42, U92, U133, U41, U91, snd, cons, isNaturalKind, U171, splitAt, U143, U201, U142, U202, U141, s, U51, tt, take, U82, U53, U81, U52, U11, afterNth, U102, sel, U103, U101, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| snd#(pair(X, Y)) | → | U181#(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) | | splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) |
| U81#(tt, V1) | → | U82#(isPLNat(V1)) | | isNaturalKind#(sel(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) |
| T(isNaturalKind(X)) | → | isNaturalKind#(X) | | snd#(pair(X, Y)) | → | and#(isLNat(X), isLNatKind(X)) |
| U11#(tt, N, XS) | → | splitAt#(N, XS) | | T(and(x_1, x_2)) | → | T(x_1) |
| tail#(cons(N, XS)) | → | isNatural#(N) | | isPLNat#(splitAt(V1, V2)) | → | isNaturalKind#(V1) |
| T(isNatural(X)) | → | isNatural#(X) | | U11#(tt, N, XS) | → | T(N) |
| U131#(tt, V1, V2) | → | isNatural#(V1) | | isLNat#(snd(V1)) | → | isPLNatKind#(V1) |
| U181#(tt, Y) | → | T(Y) | | head#(cons(N, XS)) | → | isNatural#(N) |
| isLNat#(take(V1, V2)) | → | U101#(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | U71#(tt, V1) | → | isNatural#(V1) |
| U111#(tt, V1) | → | U112#(isLNat(V1)) | | U141#(tt, V1, V2) | → | isLNat#(V1) |
| head#(cons(N, XS)) | → | and#(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))) | | U142#(tt, V2) | → | isLNat#(V2) |
| U52#(tt, V2) | → | isLNat#(V2) | | isNaturalKind#(sel(V1, V2)) | → | isNaturalKind#(V1) |
| afterNth#(N, XS) | → | and#(isNatural(N), isNaturalKind(N)) | | and#(tt, X) | → | T(X) |
| U101#(tt, V1, V2) | → | U102#(isNatural(V1), V2) | | T(isLNatKind(Y)) | → | isLNatKind#(Y) |
| isLNat#(afterNth(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) | | isPLNat#(pair(V1, V2)) | → | and#(isLNatKind(V1), isLNatKind(V2)) |
| U111#(tt, V1) | → | isLNat#(V1) | | splitAt#(0, XS) | → | and#(isLNat(XS), isLNatKind(XS)) |
| take#(N, XS) | → | and#(isNatural(N), isNaturalKind(N)) | | U201#(tt, N, X, XS) | → | T(XS) |
| U61#(tt, V1) | → | U62#(isPLNat(V1)) | | U51#(tt, V1, V2) | → | isNatural#(V1) |
| U121#(tt, V1) | → | isNatural#(V1) | | isPLNatKind#(pair(V1, V2)) | → | isLNatKind#(V1) |
| T(isNaturalKind(N)) | → | isNaturalKind#(N) | | isLNat#(natsFrom(V1)) | → | U71#(isNaturalKind(V1), V1) |
| U91#(tt, V1) | → | U92#(isLNat(V1)) | | U61#(tt, V1) | → | isPLNat#(V1) |
| sel#(N, XS) | → | and#(isNatural(N), isNaturalKind(N)) | | T(isNatural(x_1)) | → | T(x_1) |
| U132#(tt, V2) | → | U133#(isLNat(V2)) | | isLNat#(cons(V1, V2)) | → | isNaturalKind#(V1) |
| U71#(tt, V1) | → | U72#(isNatural(V1)) | | isLNatKind#(cons(V1, V2)) | → | isNaturalKind#(V1) |
| T(and(x_1, x_2)) | → | T(x_2) | | T(isLNatKind(XS)) | → | isLNatKind#(XS) |
| U221#(tt, N, XS) | → | T(N) | | U52#(tt, V2) | → | U53#(isLNat(V2)) |
| head#(cons(N, XS)) | → | and#(isNatural(N), isNaturalKind(N)) | | isPLNat#(pair(V1, V2)) | → | isLNatKind#(V1) |
| isNatural#(s(V1)) | → | U121#(isNaturalKind(V1), V1) | | afterNth#(N, XS) | → | and#(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))) |
| splitAt#(s(N), cons(X, XS)) | → | U201#(and(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) | | U221#(tt, N, XS) | → | splitAt#(N, XS) |
| isLNat#(tail(V1)) | → | isLNatKind#(V1) | | U102#(tt, V2) | → | U103#(isLNat(V2)) |
| U221#(tt, N, XS) | → | fst#(splitAt(N, XS)) | | U152#(tt, V2) | → | isLNat#(V2) |
| isLNat#(cons(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) | | U151#(tt, V1, V2) | → | isNatural#(V1) |
| U161#(tt, N) | → | T(N) | | isPLNatKind#(splitAt(V1, V2)) | → | isNaturalKind#(V1) |
| isNatural#(head(V1)) | → | isLNatKind#(V1) | | U51#(tt, V1, V2) | → | U52#(isNatural(V1), V2) |
| U121#(tt, V1) | → | U122#(isNatural(V1)) | | T(natsFrom(x_1)) | → | T(x_1) |
| isPLNat#(splitAt(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) | | U31#(tt, N) | → | T(N) |
| isNaturalKind#(s(V1)) | → | isNaturalKind#(V1) | | splitAt#(s(N), cons(X, XS)) | → | and#(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))) |
| U81#(tt, V1) | → | isPLNat#(V1) | | U41#(tt, V1, V2) | → | isNatural#(V1) |
| U21#(tt, X) | → | T(X) | | fst#(pair(X, Y)) | → | and#(isLNat(X), isLNatKind(X)) |
| U11#(tt, N, XS) | → | snd#(splitAt(N, XS)) | | take#(N, XS) | → | U221#(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
| U142#(tt, V2) | → | U143#(isLNat(V2)) | | isLNatKind#(take(V1, V2)) | → | isNaturalKind#(V1) |
| splitAt#(0, XS) | → | U191#(and(isLNat(XS), isLNatKind(XS)), XS) | | isLNat#(snd(V1)) | → | U81#(isPLNatKind(V1), V1) |
| isPLNat#(pair(V1, V2)) | → | U141#(and(isLNatKind(V1), isLNatKind(V2)), V1, V2) | | U152#(tt, V2) | → | U153#(isLNat(V2)) |
| U171#(tt, N, XS) | → | head#(afterNth(N, XS)) | | T(and(isLNat(Y), isLNatKind(Y))) | → | and#(isLNat(Y), isLNatKind(Y)) |
| U102#(tt, V2) | → | isLNat#(V2) | | U211#(tt, XS) | → | T(XS) |
| U191#(tt, XS) | → | T(XS) | | isLNatKind#(cons(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) |
| T(isLNat(XS)) | → | isLNat#(XS) | | U141#(tt, V1, V2) | → | U142#(isLNat(V1), V2) |
| isLNat#(take(V1, V2)) | → | isNaturalKind#(V1) | | isPLNatKind#(pair(V1, V2)) | → | and#(isLNatKind(V1), isLNatKind(V2)) |
| isLNatKind#(take(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) | | fst#(pair(X, Y)) | → | and#(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))) |
| T(and(isNatural(X), isNaturalKind(X))) | → | and#(isNatural(X), isNaturalKind(X)) | | isLNat#(natsFrom(V1)) | → | isNaturalKind#(V1) |
| T(and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))) | → | and#(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS))) | | U171#(tt, N, XS) | → | afterNth#(N, XS) |
| T(s(x_1)) | → | T(x_1) | | isNatural#(sel(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) |
| isNatural#(sel(V1, V2)) | → | U131#(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | T(isLNatKind(V2)) | → | isLNatKind#(V2) |
| isLNat#(afterNth(V1, V2)) | → | isNaturalKind#(V1) | | snd#(pair(X, Y)) | → | isLNat#(X) |
| splitAt#(0, XS) | → | isLNat#(XS) | | tail#(cons(N, XS)) | → | and#(isNatural(N), isNaturalKind(N)) |
| natsFrom#(N) | → | isNatural#(N) | | isLNatKind#(snd(V1)) | → | isPLNatKind#(V1) |
| T(natsFrom(s(N))) | → | natsFrom#(s(N)) | | U201#(tt, N, X, XS) | → | U202#(splitAt(N, XS), X) |
| isLNatKind#(fst(V1)) | → | isPLNatKind#(V1) | | isLNatKind#(afterNth(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) |
| head#(cons(N, XS)) | → | U31#(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) | | isNatural#(head(V1)) | → | U111#(isLNatKind(V1), V1) |
| U41#(tt, V1, V2) | → | U42#(isNatural(V1), V2) | | fst#(pair(X, Y)) | → | isLNat#(X) |
| T(and(isLNat(XS), isLNatKind(XS))) | → | and#(isLNat(XS), isLNatKind(XS)) | | sel#(N, XS) | → | isNatural#(N) |
| splitAt#(s(N), cons(X, XS)) | → | and#(isNatural(N), isNaturalKind(N)) | | tail#(cons(N, XS)) | → | U211#(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), XS) |
| natsFrom#(N) | → | U161#(and(isNatural(N), isNaturalKind(N)), N) | | take#(N, XS) | → | isNatural#(N) |
| isNaturalKind#(head(V1)) | → | isLNatKind#(V1) | | U201#(tt, N, X, XS) | → | splitAt#(N, XS) |
| U91#(tt, V1) | → | isLNat#(V1) | | isLNat#(tail(V1)) | → | U91#(isLNatKind(V1), V1) |
| snd#(pair(X, Y)) | → | and#(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))) | | U221#(tt, N, XS) | → | T(XS) |
| T(isLNatKind(X)) | → | isLNatKind#(X) | | isLNat#(take(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) |
| U151#(tt, V1, V2) | → | U152#(isNatural(V1), V2) | | T(isLNat(Y)) | → | isLNat#(Y) |
| fst#(pair(X, Y)) | → | U21#(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) | | isNatural#(sel(V1, V2)) | → | isNaturalKind#(V1) |
| isPLNatKind#(splitAt(V1, V2)) | → | and#(isNaturalKind(V1), isLNatKind(V2)) | | isNatural#(s(V1)) | → | isNaturalKind#(V1) |
| isLNat#(fst(V1)) | → | U61#(isPLNatKind(V1), V1) | | U132#(tt, V2) | → | isLNat#(V2) |
| tail#(cons(N, XS)) | → | and#(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))) | | isLNatKind#(natsFrom(V1)) | → | isNaturalKind#(V1) |
| U11#(tt, N, XS) | → | T(XS) | | isLNat#(afterNth(V1, V2)) | → | U41#(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| afterNth#(N, XS) | → | U11#(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | | U171#(tt, N, XS) | → | T(N) |
| afterNth#(N, XS) | → | isNatural#(N) | | U202#(pair(YS, ZS), X) | → | T(X) |
| T(isLNat(x_1)) | → | T(x_1) | | U42#(tt, V2) | → | U43#(isLNat(V2)) |
| isLNatKind#(tail(V1)) | → | isLNatKind#(V1) | | take#(N, XS) | → | and#(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))) |
| U131#(tt, V1, V2) | → | U132#(isNatural(V1), V2) | | T(isLNatKind(x_1)) | → | T(x_1) |
| sel#(N, XS) | → | U171#(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | | sel#(N, XS) | → | and#(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))) |
| isLNatKind#(afterNth(V1, V2)) | → | isNaturalKind#(V1) | | U171#(tt, N, XS) | → | T(XS) |
| isLNat#(cons(V1, V2)) | → | U51#(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNat#(fst(V1)) | → | isPLNatKind#(V1) |
| T(isNaturalKind(x_1)) | → | T(x_1) | | isPLNat#(splitAt(V1, V2)) | → | U151#(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| U101#(tt, V1, V2) | → | isNatural#(V1) | | U201#(tt, N, X, XS) | → | T(N) |
| natsFrom#(N) | → | and#(isNatural(N), isNaturalKind(N)) | | U42#(tt, V2) | → | isLNat#(V2) |
Rewrite Rules
| U101(tt, V1, V2) | → | U102(isNatural(V1), V2) | | U102(tt, V2) | → | U103(isLNat(V2)) |
| U103(tt) | → | tt | | U11(tt, N, XS) | → | snd(splitAt(N, XS)) |
| U111(tt, V1) | → | U112(isLNat(V1)) | | U112(tt) | → | tt |
| U121(tt, V1) | → | U122(isNatural(V1)) | | U122(tt) | → | tt |
| U131(tt, V1, V2) | → | U132(isNatural(V1), V2) | | U132(tt, V2) | → | U133(isLNat(V2)) |
| U133(tt) | → | tt | | U141(tt, V1, V2) | → | U142(isLNat(V1), V2) |
| U142(tt, V2) | → | U143(isLNat(V2)) | | U143(tt) | → | tt |
| U151(tt, V1, V2) | → | U152(isNatural(V1), V2) | | U152(tt, V2) | → | U153(isLNat(V2)) |
| U153(tt) | → | tt | | U161(tt, N) | → | cons(N, natsFrom(s(N))) |
| U171(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | Y |
| U191(tt, XS) | → | pair(nil, XS) | | U201(tt, N, X, XS) | → | U202(splitAt(N, XS), X) |
| U202(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) | | U21(tt, X) | → | X |
| U211(tt, XS) | → | XS | | U221(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N) | → | N | | U41(tt, V1, V2) | → | U42(isNatural(V1), V2) |
| U42(tt, V2) | → | U43(isLNat(V2)) | | U43(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNatural(V1), V2) | | U52(tt, V2) | → | U53(isLNat(V2)) |
| U53(tt) | → | tt | | U61(tt, V1) | → | U62(isPLNat(V1)) |
| U62(tt) | → | tt | | U71(tt, V1) | → | U72(isNatural(V1)) |
| U72(tt) | → | tt | | U81(tt, V1) | → | U82(isPLNat(V1)) |
| U82(tt) | → | tt | | U91(tt, V1) | → | U92(isLNat(V1)) |
| U92(tt) | → | tt | | afterNth(N, XS) | → | U11(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
| and(tt, X) | → | X | | fst(pair(X, Y)) | → | U21(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) |
| head(cons(N, XS)) | → | U31(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNat(cons(V1, V2)) | → | U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| isLNat(fst(V1)) | → | U61(isPLNatKind(V1), V1) | | isLNat(natsFrom(V1)) | → | U71(isNaturalKind(V1), V1) |
| isLNat(snd(V1)) | → | U81(isPLNatKind(V1), V1) | | isLNat(tail(V1)) | → | U91(isLNatKind(V1), V1) |
| isLNat(take(V1, V2)) | → | U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNatKind(nil) | → | tt |
| isLNatKind(afterNth(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isLNatKind(cons(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) |
| isLNatKind(fst(V1)) | → | isPLNatKind(V1) | | isLNatKind(natsFrom(V1)) | → | isNaturalKind(V1) |
| isLNatKind(snd(V1)) | → | isPLNatKind(V1) | | isLNatKind(tail(V1)) | → | isLNatKind(V1) |
| isLNatKind(take(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNatKind(V1), V1) | | isNatural(s(V1)) | → | U121(isNaturalKind(V1), V1) |
| isNatural(sel(V1, V2)) | → | U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isNaturalKind(0) | → | tt |
| isNaturalKind(head(V1)) | → | isLNatKind(V1) | | isNaturalKind(s(V1)) | → | isNaturalKind(V1) |
| isNaturalKind(sel(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isPLNat(pair(V1, V2)) | → | U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isPLNatKind(pair(V1, V2)) | → | and(isLNatKind(V1), isLNatKind(V2)) |
| isPLNatKind(splitAt(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | natsFrom(N) | → | U161(and(isNatural(N), isNaturalKind(N)), N) |
| sel(N, XS) | → | U171(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | | snd(pair(X, Y)) | → | U181(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) |
| splitAt(0, XS) | → | U191(and(isLNat(XS), isLNatKind(XS)), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(and(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) |
| tail(cons(N, XS)) | → | U211(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), XS) | | take(N, XS) | → | U221(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U112, fst, U111, U62, U61, U211, head, U21, U153, U151, isPLNat, U152, isLNatKind, tail, U191, U71, and, U72, U122, isPLNatKind, 0, U121, U221, isLNat, U31, U181, pair, isNatural, U132, U131, U43, U42, U92, U133, U41, U91, snd, cons, isNaturalKind, U171, splitAt, U143, U201, U142, U202, U141, U51, s, tt, U53, U82, take, U52, U81, U11, afterNth, U102, U103, sel, nil, U101
Strategy
Context-sensitive strategy:
μ(isNatural#) = μ(isNaturalKind#) = μ(isLNatKind#) = μ(isLNatKind) = μ(isPLNat) = μ(0) = μ(isLNat#) = μ(T) = μ(tt) = μ(isPLNatKind#) = μ(isPLNatKind) = μ(isLNat) = μ(isNatural) = μ(isNaturalKind) = μ(isPLNat#) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(U31#) = μ(fst#) = μ(U181#) = μ(tail#) = μ(U52#) = μ(U112) = μ(U111) = μ(U62) = μ(U61) = μ(U161#) = μ(U72#) = μ(U51#) = μ(U202#) = μ(tail) = μ(U71) = μ(U191) = μ(U72) = μ(U71#) = μ(U122) = μ(U121) = μ(U102#) = μ(and#) = μ(U122#) = μ(U201#) = μ(U221#) = μ(U43#) = μ(U132) = μ(U131) = μ(U43) = μ(U42) = μ(U133) = μ(U41) = μ(U142#) = μ(cons) = μ(U101#) = μ(U121#) = μ(U53#) = μ(U143) = μ(U142) = μ(U141) = μ(U51) = μ(s) = μ(U53) = μ(U52) = μ(U141#) = μ(U151#) = μ(natsFrom) = μ(U21#) = μ(U161) = μ(U62#) = μ(U171#) = μ(fst) = μ(U41#) = μ(U211) = μ(snd#) = μ(head) = μ(U21) = μ(U152#) = μ(U61#) = μ(U153) = μ(U103#) = μ(U151) = μ(U152) = μ(and) = μ(U42#) = μ(U133#) = μ(U143#) = μ(U191#) = μ(U221) = μ(U31) = μ(U181) = μ(U153#) = μ(U91#) = μ(U81#) = μ(U211#) = μ(U92) = μ(U91) = μ(U132#) = μ(U111#) = μ(snd) = μ(U171) = μ(U92#) = μ(U82#) = μ(U201) = μ(U202) = μ(U82) = μ(U81) = μ(U11) = μ(U112#) = μ(U131#) = μ(head#) = μ(U102) = μ(U103) = μ(U101) = {1}
μ(sel#) = μ(take#) = μ(pair) = μ(splitAt) = μ(afterNth) = μ(splitAt#) = μ(afterNth#) = μ(take) = μ(sel) = {1, 2}
The following SCCs where found
| snd#(pair(X, Y)) → and#(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))) | snd#(pair(X, Y)) → U181#(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) |
| U181#(tt, Y) → T(Y) | snd#(pair(X, Y)) → and#(isLNat(X), isLNatKind(X)) |
| U11#(tt, N, XS) → snd#(splitAt(N, XS)) |
| U31#(tt, N) → T(N) | head#(cons(N, XS)) → U31#(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) |
| head#(cons(N, XS)) → isNatural#(N) | U171#(tt, N, XS) → head#(afterNth(N, XS)) |
| head#(cons(N, XS)) → and#(isNatural(N), isNaturalKind(N)) | head#(cons(N, XS)) → and#(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))) |
| sel#(N, XS) → U171#(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | U171#(tt, N, XS) → T(XS) |
| U171#(tt, N, XS) → T(N) |
| afterNth#(N, XS) → and#(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))) | U171#(tt, N, XS) → afterNth#(N, XS) |
| afterNth#(N, XS) → isNatural#(N) |
| U201#(tt, N, X, XS) → U202#(splitAt(N, XS), X) | U202#(pair(YS, ZS), X) → T(X) |
| U11#(tt, N, XS) → T(N) | U11#(tt, N, XS) → T(XS) |
| afterNth#(N, XS) → U11#(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
| splitAt#(s(N), cons(X, XS)) → U201#(and(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) | U201#(tt, N, X, XS) → splitAt#(N, XS) |
| fst#(pair(X, Y)) → isLNat#(X) | fst#(pair(X, Y)) → U21#(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) |
| U221#(tt, N, XS) → fst#(splitAt(N, XS)) | U21#(tt, X) → T(X) |
| fst#(pair(X, Y)) → and#(isLNat(X), isLNatKind(X)) | fst#(pair(X, Y)) → and#(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))) |
| isNaturalKind#(sel(V1, V2)) → and#(isNaturalKind(V1), isLNatKind(V2)) | T(isNaturalKind(X)) → isNaturalKind#(X) |
| T(and(x_1, x_2)) → T(x_1) | isPLNat#(splitAt(V1, V2)) → isNaturalKind#(V1) |
| T(isNatural(X)) → isNatural#(X) | isLNat#(snd(V1)) → isPLNatKind#(V1) |
| U131#(tt, V1, V2) → isNatural#(V1) | isLNat#(take(V1, V2)) → U101#(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| U71#(tt, V1) → isNatural#(V1) | U141#(tt, V1, V2) → isLNat#(V1) |
| U142#(tt, V2) → isLNat#(V2) | U52#(tt, V2) → isLNat#(V2) |
| isNaturalKind#(sel(V1, V2)) → isNaturalKind#(V1) | U101#(tt, V1, V2) → U102#(isNatural(V1), V2) |
| T(isLNatKind(Y)) → isLNatKind#(Y) | and#(tt, X) → T(X) |
| isLNat#(afterNth(V1, V2)) → and#(isNaturalKind(V1), isLNatKind(V2)) | isPLNat#(pair(V1, V2)) → and#(isLNatKind(V1), isLNatKind(V2)) |
| U111#(tt, V1) → isLNat#(V1) | U51#(tt, V1, V2) → isNatural#(V1) |
| U121#(tt, V1) → isNatural#(V1) | T(isNaturalKind(N)) → isNaturalKind#(N) |
| isPLNatKind#(pair(V1, V2)) → isLNatKind#(V1) | isLNat#(natsFrom(V1)) → U71#(isNaturalKind(V1), V1) |
| U61#(tt, V1) → isPLNat#(V1) | T(isNatural(x_1)) → T(x_1) |
| isLNat#(cons(V1, V2)) → isNaturalKind#(V1) | T(and(x_1, x_2)) → T(x_2) |
| isLNatKind#(cons(V1, V2)) → isNaturalKind#(V1) | T(isLNatKind(XS)) → isLNatKind#(XS) |
| isPLNat#(pair(V1, V2)) → isLNatKind#(V1) | isNatural#(s(V1)) → U121#(isNaturalKind(V1), V1) |
| isLNat#(tail(V1)) → isLNatKind#(V1) | U152#(tt, V2) → isLNat#(V2) |
| isLNat#(cons(V1, V2)) → and#(isNaturalKind(V1), isLNatKind(V2)) | U151#(tt, V1, V2) → isNatural#(V1) |
| U161#(tt, N) → T(N) | isPLNatKind#(splitAt(V1, V2)) → isNaturalKind#(V1) |
| isNatural#(head(V1)) → isLNatKind#(V1) | U51#(tt, V1, V2) → U52#(isNatural(V1), V2) |
| isPLNat#(splitAt(V1, V2)) → and#(isNaturalKind(V1), isLNatKind(V2)) | T(natsFrom(x_1)) → T(x_1) |
| isNaturalKind#(s(V1)) → isNaturalKind#(V1) | U81#(tt, V1) → isPLNat#(V1) |
| U41#(tt, V1, V2) → isNatural#(V1) | isLNatKind#(take(V1, V2)) → isNaturalKind#(V1) |
| isLNat#(snd(V1)) → U81#(isPLNatKind(V1), V1) | isPLNat#(pair(V1, V2)) → U141#(and(isLNatKind(V1), isLNatKind(V2)), V1, V2) |
| T(and(isLNat(Y), isLNatKind(Y))) → and#(isLNat(Y), isLNatKind(Y)) | U102#(tt, V2) → isLNat#(V2) |
| isLNatKind#(cons(V1, V2)) → and#(isNaturalKind(V1), isLNatKind(V2)) | U141#(tt, V1, V2) → U142#(isLNat(V1), V2) |
| T(isLNat(XS)) → isLNat#(XS) | isLNat#(take(V1, V2)) → isNaturalKind#(V1) |
| isPLNatKind#(pair(V1, V2)) → and#(isLNatKind(V1), isLNatKind(V2)) | isLNatKind#(take(V1, V2)) → and#(isNaturalKind(V1), isLNatKind(V2)) |
| T(and(isNatural(X), isNaturalKind(X))) → and#(isNatural(X), isNaturalKind(X)) | isLNat#(natsFrom(V1)) → isNaturalKind#(V1) |
| T(and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))) → and#(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS))) | T(s(x_1)) → T(x_1) |
| isNatural#(sel(V1, V2)) → and#(isNaturalKind(V1), isLNatKind(V2)) | isNatural#(sel(V1, V2)) → U131#(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| T(isLNatKind(V2)) → isLNatKind#(V2) | isLNat#(afterNth(V1, V2)) → isNaturalKind#(V1) |
| natsFrom#(N) → isNatural#(N) | isLNatKind#(snd(V1)) → isPLNatKind#(V1) |
| T(natsFrom(s(N))) → natsFrom#(s(N)) | isLNatKind#(fst(V1)) → isPLNatKind#(V1) |
| isLNatKind#(afterNth(V1, V2)) → and#(isNaturalKind(V1), isLNatKind(V2)) | isNatural#(head(V1)) → U111#(isLNatKind(V1), V1) |
| U41#(tt, V1, V2) → U42#(isNatural(V1), V2) | T(and(isLNat(XS), isLNatKind(XS))) → and#(isLNat(XS), isLNatKind(XS)) |
| natsFrom#(N) → U161#(and(isNatural(N), isNaturalKind(N)), N) | isNaturalKind#(head(V1)) → isLNatKind#(V1) |
| U91#(tt, V1) → isLNat#(V1) | isLNat#(tail(V1)) → U91#(isLNatKind(V1), V1) |
| T(isLNatKind(X)) → isLNatKind#(X) | U151#(tt, V1, V2) → U152#(isNatural(V1), V2) |
| isLNat#(take(V1, V2)) → and#(isNaturalKind(V1), isLNatKind(V2)) | T(isLNat(Y)) → isLNat#(Y) |
| isNatural#(sel(V1, V2)) → isNaturalKind#(V1) | isPLNatKind#(splitAt(V1, V2)) → and#(isNaturalKind(V1), isLNatKind(V2)) |
| isNatural#(s(V1)) → isNaturalKind#(V1) | isLNat#(fst(V1)) → U61#(isPLNatKind(V1), V1) |
| U132#(tt, V2) → isLNat#(V2) | isLNatKind#(natsFrom(V1)) → isNaturalKind#(V1) |
| isLNat#(afterNth(V1, V2)) → U41#(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | T(isLNat(x_1)) → T(x_1) |
| isLNatKind#(tail(V1)) → isLNatKind#(V1) | U131#(tt, V1, V2) → U132#(isNatural(V1), V2) |
| T(isLNatKind(x_1)) → T(x_1) | isLNatKind#(afterNth(V1, V2)) → isNaturalKind#(V1) |
| isLNat#(cons(V1, V2)) → U51#(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | isLNat#(fst(V1)) → isPLNatKind#(V1) |
| T(isNaturalKind(x_1)) → T(x_1) | isPLNat#(splitAt(V1, V2)) → U151#(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| U101#(tt, V1, V2) → isNatural#(V1) | natsFrom#(N) → and#(isNatural(N), isNaturalKind(N)) |
| U42#(tt, V2) → isLNat#(V2) |
| snd#(pair(X, Y)) → isLNat#(X) | snd#(pair(X, Y)) → and#(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))) |
| U11#(tt, N, XS) → T(N) | snd#(pair(X, Y)) → U181#(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) |
| U181#(tt, Y) → T(Y) | snd#(pair(X, Y)) → and#(isLNat(X), isLNatKind(X)) |
| U11#(tt, N, XS) → T(XS) | afterNth#(N, XS) → U11#(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
| U11#(tt, N, XS) → snd#(splitAt(N, XS)) |
| take#(N, XS) → U221#(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | U221#(tt, N, XS) → T(XS) |
Problem 2: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| take#(N, XS) | → | U221#(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | | U221#(tt, N, XS) | → | T(XS) |
Rewrite Rules
| U101(tt, V1, V2) | → | U102(isNatural(V1), V2) | | U102(tt, V2) | → | U103(isLNat(V2)) |
| U103(tt) | → | tt | | U11(tt, N, XS) | → | snd(splitAt(N, XS)) |
| U111(tt, V1) | → | U112(isLNat(V1)) | | U112(tt) | → | tt |
| U121(tt, V1) | → | U122(isNatural(V1)) | | U122(tt) | → | tt |
| U131(tt, V1, V2) | → | U132(isNatural(V1), V2) | | U132(tt, V2) | → | U133(isLNat(V2)) |
| U133(tt) | → | tt | | U141(tt, V1, V2) | → | U142(isLNat(V1), V2) |
| U142(tt, V2) | → | U143(isLNat(V2)) | | U143(tt) | → | tt |
| U151(tt, V1, V2) | → | U152(isNatural(V1), V2) | | U152(tt, V2) | → | U153(isLNat(V2)) |
| U153(tt) | → | tt | | U161(tt, N) | → | cons(N, natsFrom(s(N))) |
| U171(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | Y |
| U191(tt, XS) | → | pair(nil, XS) | | U201(tt, N, X, XS) | → | U202(splitAt(N, XS), X) |
| U202(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) | | U21(tt, X) | → | X |
| U211(tt, XS) | → | XS | | U221(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N) | → | N | | U41(tt, V1, V2) | → | U42(isNatural(V1), V2) |
| U42(tt, V2) | → | U43(isLNat(V2)) | | U43(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNatural(V1), V2) | | U52(tt, V2) | → | U53(isLNat(V2)) |
| U53(tt) | → | tt | | U61(tt, V1) | → | U62(isPLNat(V1)) |
| U62(tt) | → | tt | | U71(tt, V1) | → | U72(isNatural(V1)) |
| U72(tt) | → | tt | | U81(tt, V1) | → | U82(isPLNat(V1)) |
| U82(tt) | → | tt | | U91(tt, V1) | → | U92(isLNat(V1)) |
| U92(tt) | → | tt | | afterNth(N, XS) | → | U11(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
| and(tt, X) | → | X | | fst(pair(X, Y)) | → | U21(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) |
| head(cons(N, XS)) | → | U31(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNat(cons(V1, V2)) | → | U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| isLNat(fst(V1)) | → | U61(isPLNatKind(V1), V1) | | isLNat(natsFrom(V1)) | → | U71(isNaturalKind(V1), V1) |
| isLNat(snd(V1)) | → | U81(isPLNatKind(V1), V1) | | isLNat(tail(V1)) | → | U91(isLNatKind(V1), V1) |
| isLNat(take(V1, V2)) | → | U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNatKind(nil) | → | tt |
| isLNatKind(afterNth(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isLNatKind(cons(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) |
| isLNatKind(fst(V1)) | → | isPLNatKind(V1) | | isLNatKind(natsFrom(V1)) | → | isNaturalKind(V1) |
| isLNatKind(snd(V1)) | → | isPLNatKind(V1) | | isLNatKind(tail(V1)) | → | isLNatKind(V1) |
| isLNatKind(take(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNatKind(V1), V1) | | isNatural(s(V1)) | → | U121(isNaturalKind(V1), V1) |
| isNatural(sel(V1, V2)) | → | U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isNaturalKind(0) | → | tt |
| isNaturalKind(head(V1)) | → | isLNatKind(V1) | | isNaturalKind(s(V1)) | → | isNaturalKind(V1) |
| isNaturalKind(sel(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isPLNat(pair(V1, V2)) | → | U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isPLNatKind(pair(V1, V2)) | → | and(isLNatKind(V1), isLNatKind(V2)) |
| isPLNatKind(splitAt(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | natsFrom(N) | → | U161(and(isNatural(N), isNaturalKind(N)), N) |
| sel(N, XS) | → | U171(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | | snd(pair(X, Y)) | → | U181(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) |
| splitAt(0, XS) | → | U191(and(isLNat(XS), isLNatKind(XS)), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(and(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) |
| tail(cons(N, XS)) | → | U211(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), XS) | | take(N, XS) | → | U221(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U112, fst, U111, U62, U61, U211, head, U21, U153, U151, isPLNat, U152, isLNatKind, tail, U191, U71, and, U72, U122, isPLNatKind, 0, U121, U221, isLNat, U31, U181, pair, isNatural, U132, U131, U43, U42, U92, U133, U41, U91, snd, cons, isNaturalKind, U171, splitAt, U143, U201, U142, U202, U141, U51, s, tt, U53, U82, take, U52, U81, U11, afterNth, U102, U103, sel, nil, U101
Strategy
Context-sensitive strategy:
μ(isNatural#) = μ(isNaturalKind#) = μ(isLNatKind#) = μ(isLNatKind) = μ(isPLNat) = μ(0) = μ(isLNat#) = μ(T) = μ(tt) = μ(isPLNatKind#) = μ(isPLNatKind) = μ(isLNat) = μ(isNatural) = μ(isNaturalKind) = μ(isPLNat#) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(fst#) = μ(U31#) = μ(U181#) = μ(U52#) = μ(tail#) = μ(U112) = μ(U111) = μ(U62) = μ(U61) = μ(U161#) = μ(U72#) = μ(U51#) = μ(U202#) = μ(tail) = μ(U71) = μ(U191) = μ(U72) = μ(U122) = μ(U71#) = μ(U121) = μ(U102#) = μ(and#) = μ(U201#) = μ(U122#) = μ(U221#) = μ(U132) = μ(U43#) = μ(U43) = μ(U131) = μ(U42) = μ(U41) = μ(U133) = μ(U142#) = μ(cons) = μ(U121#) = μ(U101#) = μ(U53#) = μ(U143) = μ(U142) = μ(U141) = μ(U51) = μ(s) = μ(U53) = μ(U52) = μ(U141#) = μ(U151#) = μ(natsFrom) = μ(U21#) = μ(U161) = μ(U62#) = μ(U171#) = μ(fst) = μ(U41#) = μ(U211) = μ(snd#) = μ(head) = μ(U21) = μ(U152#) = μ(U61#) = μ(U153) = μ(U103#) = μ(U151) = μ(U152) = μ(and) = μ(U42#) = μ(U133#) = μ(U143#) = μ(U191#) = μ(U221) = μ(U31) = μ(U181) = μ(U153#) = μ(U91#) = μ(U81#) = μ(U211#) = μ(U92) = μ(U91) = μ(U132#) = μ(U111#) = μ(snd) = μ(U171) = μ(U92#) = μ(U82#) = μ(U201) = μ(U202) = μ(U82) = μ(U81) = μ(U112#) = μ(U11) = μ(head#) = μ(U131#) = μ(U102) = μ(U103) = μ(U101) = {1}
μ(sel#) = μ(take#) = μ(pair) = μ(splitAt) = μ(afterNth) = μ(splitAt#) = μ(afterNth#) = μ(take) = μ(sel) = {1, 2}
There are no SCCs!
Problem 3: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| fst#(pair(X, Y)) | → | isLNat#(X) | | fst#(pair(X, Y)) | → | U21#(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) |
| U221#(tt, N, XS) | → | fst#(splitAt(N, XS)) | | U21#(tt, X) | → | T(X) |
| fst#(pair(X, Y)) | → | and#(isLNat(X), isLNatKind(X)) | | fst#(pair(X, Y)) | → | and#(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))) |
Rewrite Rules
| U101(tt, V1, V2) | → | U102(isNatural(V1), V2) | | U102(tt, V2) | → | U103(isLNat(V2)) |
| U103(tt) | → | tt | | U11(tt, N, XS) | → | snd(splitAt(N, XS)) |
| U111(tt, V1) | → | U112(isLNat(V1)) | | U112(tt) | → | tt |
| U121(tt, V1) | → | U122(isNatural(V1)) | | U122(tt) | → | tt |
| U131(tt, V1, V2) | → | U132(isNatural(V1), V2) | | U132(tt, V2) | → | U133(isLNat(V2)) |
| U133(tt) | → | tt | | U141(tt, V1, V2) | → | U142(isLNat(V1), V2) |
| U142(tt, V2) | → | U143(isLNat(V2)) | | U143(tt) | → | tt |
| U151(tt, V1, V2) | → | U152(isNatural(V1), V2) | | U152(tt, V2) | → | U153(isLNat(V2)) |
| U153(tt) | → | tt | | U161(tt, N) | → | cons(N, natsFrom(s(N))) |
| U171(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | Y |
| U191(tt, XS) | → | pair(nil, XS) | | U201(tt, N, X, XS) | → | U202(splitAt(N, XS), X) |
| U202(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) | | U21(tt, X) | → | X |
| U211(tt, XS) | → | XS | | U221(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N) | → | N | | U41(tt, V1, V2) | → | U42(isNatural(V1), V2) |
| U42(tt, V2) | → | U43(isLNat(V2)) | | U43(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNatural(V1), V2) | | U52(tt, V2) | → | U53(isLNat(V2)) |
| U53(tt) | → | tt | | U61(tt, V1) | → | U62(isPLNat(V1)) |
| U62(tt) | → | tt | | U71(tt, V1) | → | U72(isNatural(V1)) |
| U72(tt) | → | tt | | U81(tt, V1) | → | U82(isPLNat(V1)) |
| U82(tt) | → | tt | | U91(tt, V1) | → | U92(isLNat(V1)) |
| U92(tt) | → | tt | | afterNth(N, XS) | → | U11(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
| and(tt, X) | → | X | | fst(pair(X, Y)) | → | U21(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) |
| head(cons(N, XS)) | → | U31(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNat(cons(V1, V2)) | → | U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| isLNat(fst(V1)) | → | U61(isPLNatKind(V1), V1) | | isLNat(natsFrom(V1)) | → | U71(isNaturalKind(V1), V1) |
| isLNat(snd(V1)) | → | U81(isPLNatKind(V1), V1) | | isLNat(tail(V1)) | → | U91(isLNatKind(V1), V1) |
| isLNat(take(V1, V2)) | → | U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNatKind(nil) | → | tt |
| isLNatKind(afterNth(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isLNatKind(cons(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) |
| isLNatKind(fst(V1)) | → | isPLNatKind(V1) | | isLNatKind(natsFrom(V1)) | → | isNaturalKind(V1) |
| isLNatKind(snd(V1)) | → | isPLNatKind(V1) | | isLNatKind(tail(V1)) | → | isLNatKind(V1) |
| isLNatKind(take(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNatKind(V1), V1) | | isNatural(s(V1)) | → | U121(isNaturalKind(V1), V1) |
| isNatural(sel(V1, V2)) | → | U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isNaturalKind(0) | → | tt |
| isNaturalKind(head(V1)) | → | isLNatKind(V1) | | isNaturalKind(s(V1)) | → | isNaturalKind(V1) |
| isNaturalKind(sel(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isPLNat(pair(V1, V2)) | → | U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isPLNatKind(pair(V1, V2)) | → | and(isLNatKind(V1), isLNatKind(V2)) |
| isPLNatKind(splitAt(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | natsFrom(N) | → | U161(and(isNatural(N), isNaturalKind(N)), N) |
| sel(N, XS) | → | U171(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | | snd(pair(X, Y)) | → | U181(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) |
| splitAt(0, XS) | → | U191(and(isLNat(XS), isLNatKind(XS)), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(and(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) |
| tail(cons(N, XS)) | → | U211(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), XS) | | take(N, XS) | → | U221(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U112, fst, U111, U62, U61, U211, head, U21, U153, U151, isPLNat, U152, isLNatKind, tail, U191, U71, and, U72, U122, isPLNatKind, 0, U121, U221, isLNat, U31, U181, pair, isNatural, U132, U131, U43, U42, U92, U133, U41, U91, snd, cons, isNaturalKind, U171, splitAt, U143, U201, U142, U202, U141, U51, s, tt, U53, U82, take, U52, U81, U11, afterNth, U102, U103, sel, nil, U101
Strategy
Context-sensitive strategy:
μ(isNatural#) = μ(isNaturalKind#) = μ(isLNatKind#) = μ(isLNatKind) = μ(isPLNat) = μ(0) = μ(isLNat#) = μ(T) = μ(tt) = μ(isPLNatKind#) = μ(isPLNatKind) = μ(isLNat) = μ(isNatural) = μ(isNaturalKind) = μ(isPLNat#) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(fst#) = μ(U31#) = μ(U181#) = μ(U52#) = μ(tail#) = μ(U112) = μ(U111) = μ(U62) = μ(U61) = μ(U161#) = μ(U72#) = μ(U51#) = μ(U202#) = μ(tail) = μ(U71) = μ(U191) = μ(U72) = μ(U122) = μ(U71#) = μ(U121) = μ(U102#) = μ(and#) = μ(U201#) = μ(U122#) = μ(U221#) = μ(U132) = μ(U43#) = μ(U43) = μ(U131) = μ(U42) = μ(U41) = μ(U133) = μ(U142#) = μ(cons) = μ(U121#) = μ(U101#) = μ(U53#) = μ(U143) = μ(U142) = μ(U141) = μ(U51) = μ(s) = μ(U53) = μ(U52) = μ(U141#) = μ(U151#) = μ(natsFrom) = μ(U21#) = μ(U161) = μ(U62#) = μ(U171#) = μ(fst) = μ(U41#) = μ(U211) = μ(snd#) = μ(head) = μ(U21) = μ(U152#) = μ(U61#) = μ(U153) = μ(U103#) = μ(U151) = μ(U152) = μ(and) = μ(U42#) = μ(U133#) = μ(U143#) = μ(U191#) = μ(U221) = μ(U31) = μ(U181) = μ(U153#) = μ(U91#) = μ(U81#) = μ(U211#) = μ(U92) = μ(U91) = μ(U132#) = μ(U111#) = μ(snd) = μ(U171) = μ(U92#) = μ(U82#) = μ(U201) = μ(U202) = μ(U82) = μ(U81) = μ(U112#) = μ(U11) = μ(head#) = μ(U131#) = μ(U102) = μ(U103) = μ(U101) = {1}
μ(sel#) = μ(take#) = μ(pair) = μ(splitAt) = μ(afterNth) = μ(splitAt#) = μ(afterNth#) = μ(take) = μ(sel) = {1, 2}
There are no SCCs!
Problem 4: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U31#(tt, N) | → | T(N) | | head#(cons(N, XS)) | → | U31#(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) |
| head#(cons(N, XS)) | → | isNatural#(N) | | U171#(tt, N, XS) | → | head#(afterNth(N, XS)) |
| head#(cons(N, XS)) | → | and#(isNatural(N), isNaturalKind(N)) | | head#(cons(N, XS)) | → | and#(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))) |
| sel#(N, XS) | → | U171#(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | | U171#(tt, N, XS) | → | T(XS) |
| U171#(tt, N, XS) | → | T(N) |
Rewrite Rules
| U101(tt, V1, V2) | → | U102(isNatural(V1), V2) | | U102(tt, V2) | → | U103(isLNat(V2)) |
| U103(tt) | → | tt | | U11(tt, N, XS) | → | snd(splitAt(N, XS)) |
| U111(tt, V1) | → | U112(isLNat(V1)) | | U112(tt) | → | tt |
| U121(tt, V1) | → | U122(isNatural(V1)) | | U122(tt) | → | tt |
| U131(tt, V1, V2) | → | U132(isNatural(V1), V2) | | U132(tt, V2) | → | U133(isLNat(V2)) |
| U133(tt) | → | tt | | U141(tt, V1, V2) | → | U142(isLNat(V1), V2) |
| U142(tt, V2) | → | U143(isLNat(V2)) | | U143(tt) | → | tt |
| U151(tt, V1, V2) | → | U152(isNatural(V1), V2) | | U152(tt, V2) | → | U153(isLNat(V2)) |
| U153(tt) | → | tt | | U161(tt, N) | → | cons(N, natsFrom(s(N))) |
| U171(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | Y |
| U191(tt, XS) | → | pair(nil, XS) | | U201(tt, N, X, XS) | → | U202(splitAt(N, XS), X) |
| U202(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) | | U21(tt, X) | → | X |
| U211(tt, XS) | → | XS | | U221(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N) | → | N | | U41(tt, V1, V2) | → | U42(isNatural(V1), V2) |
| U42(tt, V2) | → | U43(isLNat(V2)) | | U43(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNatural(V1), V2) | | U52(tt, V2) | → | U53(isLNat(V2)) |
| U53(tt) | → | tt | | U61(tt, V1) | → | U62(isPLNat(V1)) |
| U62(tt) | → | tt | | U71(tt, V1) | → | U72(isNatural(V1)) |
| U72(tt) | → | tt | | U81(tt, V1) | → | U82(isPLNat(V1)) |
| U82(tt) | → | tt | | U91(tt, V1) | → | U92(isLNat(V1)) |
| U92(tt) | → | tt | | afterNth(N, XS) | → | U11(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
| and(tt, X) | → | X | | fst(pair(X, Y)) | → | U21(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) |
| head(cons(N, XS)) | → | U31(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNat(cons(V1, V2)) | → | U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| isLNat(fst(V1)) | → | U61(isPLNatKind(V1), V1) | | isLNat(natsFrom(V1)) | → | U71(isNaturalKind(V1), V1) |
| isLNat(snd(V1)) | → | U81(isPLNatKind(V1), V1) | | isLNat(tail(V1)) | → | U91(isLNatKind(V1), V1) |
| isLNat(take(V1, V2)) | → | U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNatKind(nil) | → | tt |
| isLNatKind(afterNth(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isLNatKind(cons(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) |
| isLNatKind(fst(V1)) | → | isPLNatKind(V1) | | isLNatKind(natsFrom(V1)) | → | isNaturalKind(V1) |
| isLNatKind(snd(V1)) | → | isPLNatKind(V1) | | isLNatKind(tail(V1)) | → | isLNatKind(V1) |
| isLNatKind(take(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNatKind(V1), V1) | | isNatural(s(V1)) | → | U121(isNaturalKind(V1), V1) |
| isNatural(sel(V1, V2)) | → | U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isNaturalKind(0) | → | tt |
| isNaturalKind(head(V1)) | → | isLNatKind(V1) | | isNaturalKind(s(V1)) | → | isNaturalKind(V1) |
| isNaturalKind(sel(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isPLNat(pair(V1, V2)) | → | U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isPLNatKind(pair(V1, V2)) | → | and(isLNatKind(V1), isLNatKind(V2)) |
| isPLNatKind(splitAt(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | natsFrom(N) | → | U161(and(isNatural(N), isNaturalKind(N)), N) |
| sel(N, XS) | → | U171(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | | snd(pair(X, Y)) | → | U181(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) |
| splitAt(0, XS) | → | U191(and(isLNat(XS), isLNatKind(XS)), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(and(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) |
| tail(cons(N, XS)) | → | U211(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), XS) | | take(N, XS) | → | U221(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U112, fst, U111, U62, U61, U211, head, U21, U153, U151, isPLNat, U152, isLNatKind, tail, U191, U71, and, U72, U122, isPLNatKind, 0, U121, U221, isLNat, U31, U181, pair, isNatural, U132, U131, U43, U42, U92, U133, U41, U91, snd, cons, isNaturalKind, U171, splitAt, U143, U201, U142, U202, U141, U51, s, tt, U53, U82, take, U52, U81, U11, afterNth, U102, U103, sel, nil, U101
Strategy
Context-sensitive strategy:
μ(isNatural#) = μ(isNaturalKind#) = μ(isLNatKind#) = μ(isLNatKind) = μ(isPLNat) = μ(0) = μ(isLNat#) = μ(T) = μ(tt) = μ(isPLNatKind#) = μ(isPLNatKind) = μ(isLNat) = μ(isNatural) = μ(isNaturalKind) = μ(isPLNat#) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(fst#) = μ(U31#) = μ(U181#) = μ(U52#) = μ(tail#) = μ(U112) = μ(U111) = μ(U62) = μ(U61) = μ(U161#) = μ(U72#) = μ(U51#) = μ(U202#) = μ(tail) = μ(U71) = μ(U191) = μ(U72) = μ(U122) = μ(U71#) = μ(U121) = μ(U102#) = μ(and#) = μ(U201#) = μ(U122#) = μ(U221#) = μ(U132) = μ(U43#) = μ(U43) = μ(U131) = μ(U42) = μ(U41) = μ(U133) = μ(U142#) = μ(cons) = μ(U121#) = μ(U101#) = μ(U53#) = μ(U143) = μ(U142) = μ(U141) = μ(U51) = μ(s) = μ(U53) = μ(U52) = μ(U141#) = μ(U151#) = μ(natsFrom) = μ(U21#) = μ(U161) = μ(U62#) = μ(U171#) = μ(fst) = μ(U41#) = μ(U211) = μ(snd#) = μ(head) = μ(U21) = μ(U152#) = μ(U61#) = μ(U153) = μ(U103#) = μ(U151) = μ(U152) = μ(and) = μ(U42#) = μ(U133#) = μ(U143#) = μ(U191#) = μ(U221) = μ(U31) = μ(U181) = μ(U153#) = μ(U91#) = μ(U81#) = μ(U211#) = μ(U92) = μ(U91) = μ(U132#) = μ(U111#) = μ(snd) = μ(U171) = μ(U92#) = μ(U82#) = μ(U201) = μ(U202) = μ(U82) = μ(U81) = μ(U112#) = μ(U11) = μ(head#) = μ(U131#) = μ(U102) = μ(U103) = μ(U101) = {1}
μ(sel#) = μ(take#) = μ(pair) = μ(splitAt) = μ(afterNth) = μ(splitAt#) = μ(afterNth#) = μ(take) = μ(sel) = {1, 2}
There are no SCCs!
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| snd#(pair(X, Y)) | → | and#(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))) | | snd#(pair(X, Y)) | → | U181#(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) |
| U181#(tt, Y) | → | T(Y) | | snd#(pair(X, Y)) | → | and#(isLNat(X), isLNatKind(X)) |
| U11#(tt, N, XS) | → | snd#(splitAt(N, XS)) |
Rewrite Rules
| U101(tt, V1, V2) | → | U102(isNatural(V1), V2) | | U102(tt, V2) | → | U103(isLNat(V2)) |
| U103(tt) | → | tt | | U11(tt, N, XS) | → | snd(splitAt(N, XS)) |
| U111(tt, V1) | → | U112(isLNat(V1)) | | U112(tt) | → | tt |
| U121(tt, V1) | → | U122(isNatural(V1)) | | U122(tt) | → | tt |
| U131(tt, V1, V2) | → | U132(isNatural(V1), V2) | | U132(tt, V2) | → | U133(isLNat(V2)) |
| U133(tt) | → | tt | | U141(tt, V1, V2) | → | U142(isLNat(V1), V2) |
| U142(tt, V2) | → | U143(isLNat(V2)) | | U143(tt) | → | tt |
| U151(tt, V1, V2) | → | U152(isNatural(V1), V2) | | U152(tt, V2) | → | U153(isLNat(V2)) |
| U153(tt) | → | tt | | U161(tt, N) | → | cons(N, natsFrom(s(N))) |
| U171(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | Y |
| U191(tt, XS) | → | pair(nil, XS) | | U201(tt, N, X, XS) | → | U202(splitAt(N, XS), X) |
| U202(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) | | U21(tt, X) | → | X |
| U211(tt, XS) | → | XS | | U221(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N) | → | N | | U41(tt, V1, V2) | → | U42(isNatural(V1), V2) |
| U42(tt, V2) | → | U43(isLNat(V2)) | | U43(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNatural(V1), V2) | | U52(tt, V2) | → | U53(isLNat(V2)) |
| U53(tt) | → | tt | | U61(tt, V1) | → | U62(isPLNat(V1)) |
| U62(tt) | → | tt | | U71(tt, V1) | → | U72(isNatural(V1)) |
| U72(tt) | → | tt | | U81(tt, V1) | → | U82(isPLNat(V1)) |
| U82(tt) | → | tt | | U91(tt, V1) | → | U92(isLNat(V1)) |
| U92(tt) | → | tt | | afterNth(N, XS) | → | U11(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
| and(tt, X) | → | X | | fst(pair(X, Y)) | → | U21(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) |
| head(cons(N, XS)) | → | U31(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNat(cons(V1, V2)) | → | U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| isLNat(fst(V1)) | → | U61(isPLNatKind(V1), V1) | | isLNat(natsFrom(V1)) | → | U71(isNaturalKind(V1), V1) |
| isLNat(snd(V1)) | → | U81(isPLNatKind(V1), V1) | | isLNat(tail(V1)) | → | U91(isLNatKind(V1), V1) |
| isLNat(take(V1, V2)) | → | U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNatKind(nil) | → | tt |
| isLNatKind(afterNth(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isLNatKind(cons(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) |
| isLNatKind(fst(V1)) | → | isPLNatKind(V1) | | isLNatKind(natsFrom(V1)) | → | isNaturalKind(V1) |
| isLNatKind(snd(V1)) | → | isPLNatKind(V1) | | isLNatKind(tail(V1)) | → | isLNatKind(V1) |
| isLNatKind(take(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNatKind(V1), V1) | | isNatural(s(V1)) | → | U121(isNaturalKind(V1), V1) |
| isNatural(sel(V1, V2)) | → | U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isNaturalKind(0) | → | tt |
| isNaturalKind(head(V1)) | → | isLNatKind(V1) | | isNaturalKind(s(V1)) | → | isNaturalKind(V1) |
| isNaturalKind(sel(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isPLNat(pair(V1, V2)) | → | U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isPLNatKind(pair(V1, V2)) | → | and(isLNatKind(V1), isLNatKind(V2)) |
| isPLNatKind(splitAt(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | natsFrom(N) | → | U161(and(isNatural(N), isNaturalKind(N)), N) |
| sel(N, XS) | → | U171(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | | snd(pair(X, Y)) | → | U181(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) |
| splitAt(0, XS) | → | U191(and(isLNat(XS), isLNatKind(XS)), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(and(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) |
| tail(cons(N, XS)) | → | U211(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), XS) | | take(N, XS) | → | U221(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U112, fst, U111, U62, U61, U211, head, U21, U153, U151, isPLNat, U152, isLNatKind, tail, U191, U71, and, U72, U122, isPLNatKind, 0, U121, U221, isLNat, U31, U181, pair, isNatural, U132, U131, U43, U42, U92, U133, U41, U91, snd, cons, isNaturalKind, U171, splitAt, U143, U201, U142, U202, U141, U51, s, tt, U53, U82, take, U52, U81, U11, afterNth, U102, U103, sel, nil, U101
Strategy
Context-sensitive strategy:
μ(isNatural#) = μ(isNaturalKind#) = μ(isLNatKind#) = μ(isLNatKind) = μ(isPLNat) = μ(0) = μ(isLNat#) = μ(T) = μ(tt) = μ(isPLNatKind#) = μ(isPLNatKind) = μ(isLNat) = μ(isNatural) = μ(isNaturalKind) = μ(isPLNat#) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(fst#) = μ(U31#) = μ(U181#) = μ(U52#) = μ(tail#) = μ(U112) = μ(U111) = μ(U62) = μ(U61) = μ(U161#) = μ(U72#) = μ(U51#) = μ(U202#) = μ(tail) = μ(U71) = μ(U191) = μ(U72) = μ(U122) = μ(U71#) = μ(U121) = μ(U102#) = μ(and#) = μ(U201#) = μ(U122#) = μ(U221#) = μ(U132) = μ(U43#) = μ(U43) = μ(U131) = μ(U42) = μ(U41) = μ(U133) = μ(U142#) = μ(cons) = μ(U121#) = μ(U101#) = μ(U53#) = μ(U143) = μ(U142) = μ(U141) = μ(U51) = μ(s) = μ(U53) = μ(U52) = μ(U141#) = μ(U151#) = μ(natsFrom) = μ(U21#) = μ(U161) = μ(U62#) = μ(U171#) = μ(fst) = μ(U41#) = μ(U211) = μ(snd#) = μ(head) = μ(U21) = μ(U152#) = μ(U61#) = μ(U153) = μ(U103#) = μ(U151) = μ(U152) = μ(and) = μ(U42#) = μ(U133#) = μ(U143#) = μ(U191#) = μ(U221) = μ(U31) = μ(U181) = μ(U153#) = μ(U91#) = μ(U81#) = μ(U211#) = μ(U92) = μ(U91) = μ(U132#) = μ(U111#) = μ(snd) = μ(U171) = μ(U92#) = μ(U82#) = μ(U201) = μ(U202) = μ(U82) = μ(U81) = μ(U112#) = μ(U11) = μ(head#) = μ(U131#) = μ(U102) = μ(U103) = μ(U101) = {1}
μ(sel#) = μ(take#) = μ(pair) = μ(splitAt) = μ(afterNth) = μ(splitAt#) = μ(afterNth#) = μ(take) = μ(sel) = {1, 2}
There are no SCCs!
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U201#(tt, N, X, XS) | → | U202#(splitAt(N, XS), X) | | U202#(pair(YS, ZS), X) | → | T(X) |
Rewrite Rules
| U101(tt, V1, V2) | → | U102(isNatural(V1), V2) | | U102(tt, V2) | → | U103(isLNat(V2)) |
| U103(tt) | → | tt | | U11(tt, N, XS) | → | snd(splitAt(N, XS)) |
| U111(tt, V1) | → | U112(isLNat(V1)) | | U112(tt) | → | tt |
| U121(tt, V1) | → | U122(isNatural(V1)) | | U122(tt) | → | tt |
| U131(tt, V1, V2) | → | U132(isNatural(V1), V2) | | U132(tt, V2) | → | U133(isLNat(V2)) |
| U133(tt) | → | tt | | U141(tt, V1, V2) | → | U142(isLNat(V1), V2) |
| U142(tt, V2) | → | U143(isLNat(V2)) | | U143(tt) | → | tt |
| U151(tt, V1, V2) | → | U152(isNatural(V1), V2) | | U152(tt, V2) | → | U153(isLNat(V2)) |
| U153(tt) | → | tt | | U161(tt, N) | → | cons(N, natsFrom(s(N))) |
| U171(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | Y |
| U191(tt, XS) | → | pair(nil, XS) | | U201(tt, N, X, XS) | → | U202(splitAt(N, XS), X) |
| U202(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) | | U21(tt, X) | → | X |
| U211(tt, XS) | → | XS | | U221(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N) | → | N | | U41(tt, V1, V2) | → | U42(isNatural(V1), V2) |
| U42(tt, V2) | → | U43(isLNat(V2)) | | U43(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNatural(V1), V2) | | U52(tt, V2) | → | U53(isLNat(V2)) |
| U53(tt) | → | tt | | U61(tt, V1) | → | U62(isPLNat(V1)) |
| U62(tt) | → | tt | | U71(tt, V1) | → | U72(isNatural(V1)) |
| U72(tt) | → | tt | | U81(tt, V1) | → | U82(isPLNat(V1)) |
| U82(tt) | → | tt | | U91(tt, V1) | → | U92(isLNat(V1)) |
| U92(tt) | → | tt | | afterNth(N, XS) | → | U11(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
| and(tt, X) | → | X | | fst(pair(X, Y)) | → | U21(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) |
| head(cons(N, XS)) | → | U31(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNat(cons(V1, V2)) | → | U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| isLNat(fst(V1)) | → | U61(isPLNatKind(V1), V1) | | isLNat(natsFrom(V1)) | → | U71(isNaturalKind(V1), V1) |
| isLNat(snd(V1)) | → | U81(isPLNatKind(V1), V1) | | isLNat(tail(V1)) | → | U91(isLNatKind(V1), V1) |
| isLNat(take(V1, V2)) | → | U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNatKind(nil) | → | tt |
| isLNatKind(afterNth(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isLNatKind(cons(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) |
| isLNatKind(fst(V1)) | → | isPLNatKind(V1) | | isLNatKind(natsFrom(V1)) | → | isNaturalKind(V1) |
| isLNatKind(snd(V1)) | → | isPLNatKind(V1) | | isLNatKind(tail(V1)) | → | isLNatKind(V1) |
| isLNatKind(take(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNatKind(V1), V1) | | isNatural(s(V1)) | → | U121(isNaturalKind(V1), V1) |
| isNatural(sel(V1, V2)) | → | U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isNaturalKind(0) | → | tt |
| isNaturalKind(head(V1)) | → | isLNatKind(V1) | | isNaturalKind(s(V1)) | → | isNaturalKind(V1) |
| isNaturalKind(sel(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isPLNat(pair(V1, V2)) | → | U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isPLNatKind(pair(V1, V2)) | → | and(isLNatKind(V1), isLNatKind(V2)) |
| isPLNatKind(splitAt(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | natsFrom(N) | → | U161(and(isNatural(N), isNaturalKind(N)), N) |
| sel(N, XS) | → | U171(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | | snd(pair(X, Y)) | → | U181(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) |
| splitAt(0, XS) | → | U191(and(isLNat(XS), isLNatKind(XS)), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(and(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) |
| tail(cons(N, XS)) | → | U211(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), XS) | | take(N, XS) | → | U221(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U112, fst, U111, U62, U61, U211, head, U21, U153, U151, isPLNat, U152, isLNatKind, tail, U191, U71, and, U72, U122, isPLNatKind, 0, U121, U221, isLNat, U31, U181, pair, isNatural, U132, U131, U43, U42, U92, U133, U41, U91, snd, cons, isNaturalKind, U171, splitAt, U143, U201, U142, U202, U141, U51, s, tt, U53, U82, take, U52, U81, U11, afterNth, U102, U103, sel, nil, U101
Strategy
Context-sensitive strategy:
μ(isNatural#) = μ(isNaturalKind#) = μ(isLNatKind#) = μ(isLNatKind) = μ(isPLNat) = μ(0) = μ(isLNat#) = μ(T) = μ(tt) = μ(isPLNatKind#) = μ(isPLNatKind) = μ(isLNat) = μ(isNatural) = μ(isNaturalKind) = μ(isPLNat#) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(fst#) = μ(U31#) = μ(U181#) = μ(U52#) = μ(tail#) = μ(U112) = μ(U111) = μ(U62) = μ(U61) = μ(U161#) = μ(U72#) = μ(U51#) = μ(U202#) = μ(tail) = μ(U71) = μ(U191) = μ(U72) = μ(U122) = μ(U71#) = μ(U121) = μ(U102#) = μ(and#) = μ(U201#) = μ(U122#) = μ(U221#) = μ(U132) = μ(U43#) = μ(U43) = μ(U131) = μ(U42) = μ(U41) = μ(U133) = μ(U142#) = μ(cons) = μ(U121#) = μ(U101#) = μ(U53#) = μ(U143) = μ(U142) = μ(U141) = μ(U51) = μ(s) = μ(U53) = μ(U52) = μ(U141#) = μ(U151#) = μ(natsFrom) = μ(U21#) = μ(U161) = μ(U62#) = μ(U171#) = μ(fst) = μ(U41#) = μ(U211) = μ(snd#) = μ(head) = μ(U21) = μ(U152#) = μ(U61#) = μ(U153) = μ(U103#) = μ(U151) = μ(U152) = μ(and) = μ(U42#) = μ(U133#) = μ(U143#) = μ(U191#) = μ(U221) = μ(U31) = μ(U181) = μ(U153#) = μ(U91#) = μ(U81#) = μ(U211#) = μ(U92) = μ(U91) = μ(U132#) = μ(U111#) = μ(snd) = μ(U171) = μ(U92#) = μ(U82#) = μ(U201) = μ(U202) = μ(U82) = μ(U81) = μ(U112#) = μ(U11) = μ(head#) = μ(U131#) = μ(U102) = μ(U103) = μ(U101) = {1}
μ(sel#) = μ(take#) = μ(pair) = μ(splitAt) = μ(afterNth) = μ(splitAt#) = μ(afterNth#) = μ(take) = μ(sel) = {1, 2}
There are no SCCs!
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| afterNth#(N, XS) | → | and#(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))) | | U171#(tt, N, XS) | → | afterNth#(N, XS) |
| afterNth#(N, XS) | → | isNatural#(N) |
Rewrite Rules
| U101(tt, V1, V2) | → | U102(isNatural(V1), V2) | | U102(tt, V2) | → | U103(isLNat(V2)) |
| U103(tt) | → | tt | | U11(tt, N, XS) | → | snd(splitAt(N, XS)) |
| U111(tt, V1) | → | U112(isLNat(V1)) | | U112(tt) | → | tt |
| U121(tt, V1) | → | U122(isNatural(V1)) | | U122(tt) | → | tt |
| U131(tt, V1, V2) | → | U132(isNatural(V1), V2) | | U132(tt, V2) | → | U133(isLNat(V2)) |
| U133(tt) | → | tt | | U141(tt, V1, V2) | → | U142(isLNat(V1), V2) |
| U142(tt, V2) | → | U143(isLNat(V2)) | | U143(tt) | → | tt |
| U151(tt, V1, V2) | → | U152(isNatural(V1), V2) | | U152(tt, V2) | → | U153(isLNat(V2)) |
| U153(tt) | → | tt | | U161(tt, N) | → | cons(N, natsFrom(s(N))) |
| U171(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | Y |
| U191(tt, XS) | → | pair(nil, XS) | | U201(tt, N, X, XS) | → | U202(splitAt(N, XS), X) |
| U202(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) | | U21(tt, X) | → | X |
| U211(tt, XS) | → | XS | | U221(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N) | → | N | | U41(tt, V1, V2) | → | U42(isNatural(V1), V2) |
| U42(tt, V2) | → | U43(isLNat(V2)) | | U43(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNatural(V1), V2) | | U52(tt, V2) | → | U53(isLNat(V2)) |
| U53(tt) | → | tt | | U61(tt, V1) | → | U62(isPLNat(V1)) |
| U62(tt) | → | tt | | U71(tt, V1) | → | U72(isNatural(V1)) |
| U72(tt) | → | tt | | U81(tt, V1) | → | U82(isPLNat(V1)) |
| U82(tt) | → | tt | | U91(tt, V1) | → | U92(isLNat(V1)) |
| U92(tt) | → | tt | | afterNth(N, XS) | → | U11(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
| and(tt, X) | → | X | | fst(pair(X, Y)) | → | U21(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) |
| head(cons(N, XS)) | → | U31(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNat(cons(V1, V2)) | → | U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| isLNat(fst(V1)) | → | U61(isPLNatKind(V1), V1) | | isLNat(natsFrom(V1)) | → | U71(isNaturalKind(V1), V1) |
| isLNat(snd(V1)) | → | U81(isPLNatKind(V1), V1) | | isLNat(tail(V1)) | → | U91(isLNatKind(V1), V1) |
| isLNat(take(V1, V2)) | → | U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNatKind(nil) | → | tt |
| isLNatKind(afterNth(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isLNatKind(cons(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) |
| isLNatKind(fst(V1)) | → | isPLNatKind(V1) | | isLNatKind(natsFrom(V1)) | → | isNaturalKind(V1) |
| isLNatKind(snd(V1)) | → | isPLNatKind(V1) | | isLNatKind(tail(V1)) | → | isLNatKind(V1) |
| isLNatKind(take(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNatKind(V1), V1) | | isNatural(s(V1)) | → | U121(isNaturalKind(V1), V1) |
| isNatural(sel(V1, V2)) | → | U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isNaturalKind(0) | → | tt |
| isNaturalKind(head(V1)) | → | isLNatKind(V1) | | isNaturalKind(s(V1)) | → | isNaturalKind(V1) |
| isNaturalKind(sel(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isPLNat(pair(V1, V2)) | → | U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isPLNatKind(pair(V1, V2)) | → | and(isLNatKind(V1), isLNatKind(V2)) |
| isPLNatKind(splitAt(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | natsFrom(N) | → | U161(and(isNatural(N), isNaturalKind(N)), N) |
| sel(N, XS) | → | U171(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | | snd(pair(X, Y)) | → | U181(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) |
| splitAt(0, XS) | → | U191(and(isLNat(XS), isLNatKind(XS)), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(and(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) |
| tail(cons(N, XS)) | → | U211(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), XS) | | take(N, XS) | → | U221(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U112, fst, U111, U62, U61, U211, head, U21, U153, U151, isPLNat, U152, isLNatKind, tail, U191, U71, and, U72, U122, isPLNatKind, 0, U121, U221, isLNat, U31, U181, pair, isNatural, U132, U131, U43, U42, U92, U133, U41, U91, snd, cons, isNaturalKind, U171, splitAt, U143, U201, U142, U202, U141, U51, s, tt, U53, U82, take, U52, U81, U11, afterNth, U102, U103, sel, nil, U101
Strategy
Context-sensitive strategy:
μ(isNatural#) = μ(isNaturalKind#) = μ(isLNatKind#) = μ(isLNatKind) = μ(isPLNat) = μ(0) = μ(isLNat#) = μ(T) = μ(tt) = μ(isPLNatKind#) = μ(isPLNatKind) = μ(isLNat) = μ(isNatural) = μ(isNaturalKind) = μ(isPLNat#) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(fst#) = μ(U31#) = μ(U181#) = μ(U52#) = μ(tail#) = μ(U112) = μ(U111) = μ(U62) = μ(U61) = μ(U161#) = μ(U72#) = μ(U51#) = μ(U202#) = μ(tail) = μ(U71) = μ(U191) = μ(U72) = μ(U122) = μ(U71#) = μ(U121) = μ(U102#) = μ(and#) = μ(U201#) = μ(U122#) = μ(U221#) = μ(U132) = μ(U43#) = μ(U43) = μ(U131) = μ(U42) = μ(U41) = μ(U133) = μ(U142#) = μ(cons) = μ(U121#) = μ(U101#) = μ(U53#) = μ(U143) = μ(U142) = μ(U141) = μ(U51) = μ(s) = μ(U53) = μ(U52) = μ(U141#) = μ(U151#) = μ(natsFrom) = μ(U21#) = μ(U161) = μ(U62#) = μ(U171#) = μ(fst) = μ(U41#) = μ(U211) = μ(snd#) = μ(head) = μ(U21) = μ(U152#) = μ(U61#) = μ(U153) = μ(U103#) = μ(U151) = μ(U152) = μ(and) = μ(U42#) = μ(U133#) = μ(U143#) = μ(U191#) = μ(U221) = μ(U31) = μ(U181) = μ(U153#) = μ(U91#) = μ(U81#) = μ(U211#) = μ(U92) = μ(U91) = μ(U132#) = μ(U111#) = μ(snd) = μ(U171) = μ(U92#) = μ(U82#) = μ(U201) = μ(U202) = μ(U82) = μ(U81) = μ(U112#) = μ(U11) = μ(head#) = μ(U131#) = μ(U102) = μ(U103) = μ(U101) = {1}
μ(sel#) = μ(take#) = μ(pair) = μ(splitAt) = μ(afterNth) = μ(splitAt#) = μ(afterNth#) = μ(take) = μ(sel) = {1, 2}
There are no SCCs!
Problem 9: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| snd#(pair(X, Y)) | → | isLNat#(X) | | snd#(pair(X, Y)) | → | and#(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))) |
| U11#(tt, N, XS) | → | T(N) | | snd#(pair(X, Y)) | → | U181#(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) |
| U181#(tt, Y) | → | T(Y) | | snd#(pair(X, Y)) | → | and#(isLNat(X), isLNatKind(X)) |
| U11#(tt, N, XS) | → | T(XS) | | afterNth#(N, XS) | → | U11#(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
| U11#(tt, N, XS) | → | snd#(splitAt(N, XS)) |
Rewrite Rules
| U101(tt, V1, V2) | → | U102(isNatural(V1), V2) | | U102(tt, V2) | → | U103(isLNat(V2)) |
| U103(tt) | → | tt | | U11(tt, N, XS) | → | snd(splitAt(N, XS)) |
| U111(tt, V1) | → | U112(isLNat(V1)) | | U112(tt) | → | tt |
| U121(tt, V1) | → | U122(isNatural(V1)) | | U122(tt) | → | tt |
| U131(tt, V1, V2) | → | U132(isNatural(V1), V2) | | U132(tt, V2) | → | U133(isLNat(V2)) |
| U133(tt) | → | tt | | U141(tt, V1, V2) | → | U142(isLNat(V1), V2) |
| U142(tt, V2) | → | U143(isLNat(V2)) | | U143(tt) | → | tt |
| U151(tt, V1, V2) | → | U152(isNatural(V1), V2) | | U152(tt, V2) | → | U153(isLNat(V2)) |
| U153(tt) | → | tt | | U161(tt, N) | → | cons(N, natsFrom(s(N))) |
| U171(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | Y |
| U191(tt, XS) | → | pair(nil, XS) | | U201(tt, N, X, XS) | → | U202(splitAt(N, XS), X) |
| U202(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) | | U21(tt, X) | → | X |
| U211(tt, XS) | → | XS | | U221(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N) | → | N | | U41(tt, V1, V2) | → | U42(isNatural(V1), V2) |
| U42(tt, V2) | → | U43(isLNat(V2)) | | U43(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNatural(V1), V2) | | U52(tt, V2) | → | U53(isLNat(V2)) |
| U53(tt) | → | tt | | U61(tt, V1) | → | U62(isPLNat(V1)) |
| U62(tt) | → | tt | | U71(tt, V1) | → | U72(isNatural(V1)) |
| U72(tt) | → | tt | | U81(tt, V1) | → | U82(isPLNat(V1)) |
| U82(tt) | → | tt | | U91(tt, V1) | → | U92(isLNat(V1)) |
| U92(tt) | → | tt | | afterNth(N, XS) | → | U11(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
| and(tt, X) | → | X | | fst(pair(X, Y)) | → | U21(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) |
| head(cons(N, XS)) | → | U31(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNat(cons(V1, V2)) | → | U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| isLNat(fst(V1)) | → | U61(isPLNatKind(V1), V1) | | isLNat(natsFrom(V1)) | → | U71(isNaturalKind(V1), V1) |
| isLNat(snd(V1)) | → | U81(isPLNatKind(V1), V1) | | isLNat(tail(V1)) | → | U91(isLNatKind(V1), V1) |
| isLNat(take(V1, V2)) | → | U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNatKind(nil) | → | tt |
| isLNatKind(afterNth(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isLNatKind(cons(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) |
| isLNatKind(fst(V1)) | → | isPLNatKind(V1) | | isLNatKind(natsFrom(V1)) | → | isNaturalKind(V1) |
| isLNatKind(snd(V1)) | → | isPLNatKind(V1) | | isLNatKind(tail(V1)) | → | isLNatKind(V1) |
| isLNatKind(take(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNatKind(V1), V1) | | isNatural(s(V1)) | → | U121(isNaturalKind(V1), V1) |
| isNatural(sel(V1, V2)) | → | U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isNaturalKind(0) | → | tt |
| isNaturalKind(head(V1)) | → | isLNatKind(V1) | | isNaturalKind(s(V1)) | → | isNaturalKind(V1) |
| isNaturalKind(sel(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isPLNat(pair(V1, V2)) | → | U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isPLNatKind(pair(V1, V2)) | → | and(isLNatKind(V1), isLNatKind(V2)) |
| isPLNatKind(splitAt(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | natsFrom(N) | → | U161(and(isNatural(N), isNaturalKind(N)), N) |
| sel(N, XS) | → | U171(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | | snd(pair(X, Y)) | → | U181(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) |
| splitAt(0, XS) | → | U191(and(isLNat(XS), isLNatKind(XS)), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(and(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) |
| tail(cons(N, XS)) | → | U211(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), XS) | | take(N, XS) | → | U221(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U112, fst, U111, U62, U61, U211, head, U21, U153, U151, isPLNat, U152, isLNatKind, tail, U191, U71, and, U72, U122, isPLNatKind, 0, U121, U221, isLNat, U31, U181, pair, isNatural, U132, U131, U43, U42, U92, U133, U41, U91, snd, cons, isNaturalKind, U171, splitAt, U143, U201, U142, U202, U141, U51, s, tt, U53, U82, take, U52, U81, U11, afterNth, U102, U103, sel, nil, U101
Strategy
Context-sensitive strategy:
μ(isNatural#) = μ(isNaturalKind#) = μ(isLNatKind#) = μ(isLNatKind) = μ(isPLNat) = μ(0) = μ(isLNat#) = μ(T) = μ(tt) = μ(isPLNatKind#) = μ(isPLNatKind) = μ(isLNat) = μ(isNatural) = μ(isNaturalKind) = μ(isPLNat#) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(fst#) = μ(U31#) = μ(U181#) = μ(U52#) = μ(tail#) = μ(U112) = μ(U111) = μ(U62) = μ(U61) = μ(U161#) = μ(U72#) = μ(U51#) = μ(U202#) = μ(tail) = μ(U71) = μ(U191) = μ(U72) = μ(U122) = μ(U71#) = μ(U121) = μ(U102#) = μ(and#) = μ(U201#) = μ(U122#) = μ(U221#) = μ(U132) = μ(U43#) = μ(U43) = μ(U131) = μ(U42) = μ(U41) = μ(U133) = μ(U142#) = μ(cons) = μ(U121#) = μ(U101#) = μ(U53#) = μ(U143) = μ(U142) = μ(U141) = μ(U51) = μ(s) = μ(U53) = μ(U52) = μ(U141#) = μ(U151#) = μ(natsFrom) = μ(U21#) = μ(U161) = μ(U62#) = μ(U171#) = μ(fst) = μ(U41#) = μ(U211) = μ(snd#) = μ(head) = μ(U21) = μ(U152#) = μ(U61#) = μ(U153) = μ(U103#) = μ(U151) = μ(U152) = μ(and) = μ(U42#) = μ(U133#) = μ(U143#) = μ(U191#) = μ(U221) = μ(U31) = μ(U181) = μ(U153#) = μ(U91#) = μ(U81#) = μ(U211#) = μ(U92) = μ(U91) = μ(U132#) = μ(U111#) = μ(snd) = μ(U171) = μ(U92#) = μ(U82#) = μ(U201) = μ(U202) = μ(U82) = μ(U81) = μ(U112#) = μ(U11) = μ(head#) = μ(U131#) = μ(U102) = μ(U103) = μ(U101) = {1}
μ(sel#) = μ(take#) = μ(pair) = μ(splitAt) = μ(afterNth) = μ(splitAt#) = μ(afterNth#) = μ(take) = μ(sel) = {1, 2}
There are no SCCs!
Problem 11: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U11#(tt, N, XS) | → | T(N) | | U11#(tt, N, XS) | → | T(XS) |
| afterNth#(N, XS) | → | U11#(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
Rewrite Rules
| U101(tt, V1, V2) | → | U102(isNatural(V1), V2) | | U102(tt, V2) | → | U103(isLNat(V2)) |
| U103(tt) | → | tt | | U11(tt, N, XS) | → | snd(splitAt(N, XS)) |
| U111(tt, V1) | → | U112(isLNat(V1)) | | U112(tt) | → | tt |
| U121(tt, V1) | → | U122(isNatural(V1)) | | U122(tt) | → | tt |
| U131(tt, V1, V2) | → | U132(isNatural(V1), V2) | | U132(tt, V2) | → | U133(isLNat(V2)) |
| U133(tt) | → | tt | | U141(tt, V1, V2) | → | U142(isLNat(V1), V2) |
| U142(tt, V2) | → | U143(isLNat(V2)) | | U143(tt) | → | tt |
| U151(tt, V1, V2) | → | U152(isNatural(V1), V2) | | U152(tt, V2) | → | U153(isLNat(V2)) |
| U153(tt) | → | tt | | U161(tt, N) | → | cons(N, natsFrom(s(N))) |
| U171(tt, N, XS) | → | head(afterNth(N, XS)) | | U181(tt, Y) | → | Y |
| U191(tt, XS) | → | pair(nil, XS) | | U201(tt, N, X, XS) | → | U202(splitAt(N, XS), X) |
| U202(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) | | U21(tt, X) | → | X |
| U211(tt, XS) | → | XS | | U221(tt, N, XS) | → | fst(splitAt(N, XS)) |
| U31(tt, N) | → | N | | U41(tt, V1, V2) | → | U42(isNatural(V1), V2) |
| U42(tt, V2) | → | U43(isLNat(V2)) | | U43(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNatural(V1), V2) | | U52(tt, V2) | → | U53(isLNat(V2)) |
| U53(tt) | → | tt | | U61(tt, V1) | → | U62(isPLNat(V1)) |
| U62(tt) | → | tt | | U71(tt, V1) | → | U72(isNatural(V1)) |
| U72(tt) | → | tt | | U81(tt, V1) | → | U82(isPLNat(V1)) |
| U82(tt) | → | tt | | U91(tt, V1) | → | U92(isLNat(V1)) |
| U92(tt) | → | tt | | afterNth(N, XS) | → | U11(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
| and(tt, X) | → | X | | fst(pair(X, Y)) | → | U21(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) |
| head(cons(N, XS)) | → | U31(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNat(cons(V1, V2)) | → | U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) |
| isLNat(fst(V1)) | → | U61(isPLNatKind(V1), V1) | | isLNat(natsFrom(V1)) | → | U71(isNaturalKind(V1), V1) |
| isLNat(snd(V1)) | → | U81(isPLNatKind(V1), V1) | | isLNat(tail(V1)) | → | U91(isLNatKind(V1), V1) |
| isLNat(take(V1, V2)) | → | U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isLNatKind(nil) | → | tt |
| isLNatKind(afterNth(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isLNatKind(cons(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) |
| isLNatKind(fst(V1)) | → | isPLNatKind(V1) | | isLNatKind(natsFrom(V1)) | → | isNaturalKind(V1) |
| isLNatKind(snd(V1)) | → | isPLNatKind(V1) | | isLNatKind(tail(V1)) | → | isLNatKind(V1) |
| isLNatKind(take(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | U111(isLNatKind(V1), V1) | | isNatural(s(V1)) | → | U121(isNaturalKind(V1), V1) |
| isNatural(sel(V1, V2)) | → | U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isNaturalKind(0) | → | tt |
| isNaturalKind(head(V1)) | → | isLNatKind(V1) | | isNaturalKind(s(V1)) | → | isNaturalKind(V1) |
| isNaturalKind(sel(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | isPLNat(pair(V1, V2)) | → | U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2) |
| isPLNat(splitAt(V1, V2)) | → | U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2) | | isPLNatKind(pair(V1, V2)) | → | and(isLNatKind(V1), isLNatKind(V2)) |
| isPLNatKind(splitAt(V1, V2)) | → | and(isNaturalKind(V1), isLNatKind(V2)) | | natsFrom(N) | → | U161(and(isNatural(N), isNaturalKind(N)), N) |
| sel(N, XS) | → | U171(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | | snd(pair(X, Y)) | → | U181(and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) |
| splitAt(0, XS) | → | U191(and(isLNat(XS), isLNatKind(XS)), XS) | | splitAt(s(N), cons(X, XS)) | → | U201(and(and(isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) |
| tail(cons(N, XS)) | → | U211(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), XS) | | take(N, XS) | → | U221(and(and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) |
Original Signature
Termination of terms over the following signature is verified: natsFrom, U161, U112, fst, U111, U62, U61, U211, head, U21, U153, U151, isPLNat, U152, isLNatKind, tail, U191, U71, and, U72, U122, isPLNatKind, 0, U121, U221, isLNat, U31, U181, pair, isNatural, U132, U131, U43, U42, U92, U133, U41, U91, snd, cons, isNaturalKind, U171, splitAt, U143, U201, U142, U202, U141, U51, s, tt, U53, U82, take, U52, U81, U11, afterNth, U102, U103, sel, nil, U101
Strategy
Context-sensitive strategy:
μ(isNatural#) = μ(isNaturalKind#) = μ(isLNatKind#) = μ(isLNatKind) = μ(isPLNat) = μ(0) = μ(isLNat#) = μ(T) = μ(tt) = μ(isPLNatKind#) = μ(isPLNatKind) = μ(isLNat) = μ(isNatural) = μ(isNaturalKind) = μ(isPLNat#) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(fst#) = μ(U31#) = μ(U181#) = μ(U52#) = μ(tail#) = μ(U112) = μ(U111) = μ(U62) = μ(U61) = μ(U161#) = μ(U72#) = μ(U51#) = μ(U202#) = μ(tail) = μ(U71) = μ(U191) = μ(U72) = μ(U122) = μ(U71#) = μ(U121) = μ(U102#) = μ(and#) = μ(U201#) = μ(U122#) = μ(U221#) = μ(U132) = μ(U43#) = μ(U43) = μ(U131) = μ(U42) = μ(U41) = μ(U133) = μ(U142#) = μ(cons) = μ(U121#) = μ(U101#) = μ(U53#) = μ(U143) = μ(U142) = μ(U141) = μ(U51) = μ(s) = μ(U53) = μ(U52) = μ(U141#) = μ(U151#) = μ(natsFrom) = μ(U21#) = μ(U161) = μ(U62#) = μ(U171#) = μ(fst) = μ(U41#) = μ(U211) = μ(snd#) = μ(head) = μ(U21) = μ(U152#) = μ(U61#) = μ(U153) = μ(U103#) = μ(U151) = μ(U152) = μ(and) = μ(U42#) = μ(U133#) = μ(U143#) = μ(U191#) = μ(U221) = μ(U31) = μ(U181) = μ(U153#) = μ(U91#) = μ(U81#) = μ(U211#) = μ(U92) = μ(U91) = μ(U132#) = μ(U111#) = μ(snd) = μ(U171) = μ(U92#) = μ(U82#) = μ(U201) = μ(U202) = μ(U82) = μ(U81) = μ(U112#) = μ(U11) = μ(head#) = μ(U131#) = μ(U102) = μ(U103) = μ(U101) = {1}
μ(sel#) = μ(take#) = μ(pair) = μ(splitAt) = μ(afterNth) = μ(splitAt#) = μ(afterNth#) = μ(take) = μ(sel) = {1, 2}
There are no SCCs!