YES
The TRS could be proven terminating. The proof took 1379 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (641ms).
| – Problem 2 was processed with processor SubtermCriterion (0ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (651ms).
| | – Problem 4 was processed with processor DependencyGraph (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | | U81#(tt, N, XS) | → | activate#(N) |
| U61#(tt, N, X, XS) | → | activate#(XS) | | U41#(tt, N, XS) | → | activate#(N) |
| U31#(tt, N) | → | U32#(tt, activate(N)) | | U62#(tt, N, X, XS) | → | activate#(XS) |
| U82#(tt, N, XS) | → | activate#(N) | | take#(N, XS) | → | U81#(tt, N, XS) |
| U51#(tt, Y) | → | U52#(tt, activate(Y)) | | U12#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) |
| U11#(tt, N, XS) | → | U12#(tt, activate(N), activate(XS)) | | U82#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) |
| U42#(tt, N, XS) | → | activate#(N) | | U42#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) |
| U42#(tt, N, XS) | → | activate#(XS) | | U21#(tt, X) | → | U22#(tt, activate(X)) |
| activate#(n__natsFrom(X)) | → | activate#(X) | | U81#(tt, N, XS) | → | U82#(tt, activate(N), activate(XS)) |
| tail#(cons(N, XS)) | → | U71#(tt, activate(XS)) | | U63#(tt, N, X, XS) | → | activate#(XS) |
| snd#(pair(X, Y)) | → | U51#(tt, Y) | | U12#(tt, N, XS) | → | activate#(N) |
| U62#(tt, N, X, XS) | → | activate#(X) | | U52#(tt, Y) | → | activate#(Y) |
| U61#(tt, N, X, XS) | → | U62#(tt, activate(N), activate(X), activate(XS)) | | fst#(pair(X, Y)) | → | U21#(tt, X) |
| U72#(tt, XS) | → | activate#(XS) | | U62#(tt, N, X, XS) | → | activate#(N) |
| U61#(tt, N, X, XS) | → | activate#(N) | | activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) |
| splitAt#(s(N), cons(X, XS)) | → | U61#(tt, N, X, activate(XS)) | | activate#(n__s(X)) | → | activate#(X) |
| tail#(cons(N, XS)) | → | activate#(XS) | | U21#(tt, X) | → | activate#(X) |
| U71#(tt, XS) | → | U72#(tt, activate(XS)) | | afterNth#(N, XS) | → | U11#(tt, N, XS) |
| U51#(tt, Y) | → | activate#(Y) | | U41#(tt, N, XS) | → | U42#(tt, activate(N), activate(XS)) |
| U42#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | | sel#(N, XS) | → | U41#(tt, N, XS) |
| U82#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | | U11#(tt, N, XS) | → | activate#(N) |
| head#(cons(N, XS)) | → | U31#(tt, N) | | U63#(tt, N, X, XS) | → | U64#(splitAt(activate(N), activate(XS)), activate(X)) |
| U82#(tt, N, XS) | → | activate#(XS) | | U32#(tt, N) | → | activate#(N) |
| U61#(tt, N, X, XS) | → | activate#(X) | | U63#(tt, N, X, XS) | → | activate#(X) |
| U81#(tt, N, XS) | → | activate#(XS) | | U31#(tt, N) | → | activate#(N) |
| U64#(pair(YS, ZS), X) | → | activate#(X) | | U12#(tt, N, XS) | → | activate#(XS) |
| U12#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | | U71#(tt, XS) | → | activate#(XS) |
| U11#(tt, N, XS) | → | activate#(XS) | | U63#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) |
| U62#(tt, N, X, XS) | → | U63#(tt, activate(N), activate(X), activate(XS)) | | U22#(tt, X) | → | activate#(X) |
| U63#(tt, N, X, XS) | → | activate#(N) | | activate#(n__s(X)) | → | s#(activate(X)) |
| U41#(tt, N, XS) | → | activate#(XS) |
Rewrite Rules
| U11(tt, N, XS) | → | U12(tt, activate(N), activate(XS)) | | U12(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) |
| U21(tt, X) | → | U22(tt, activate(X)) | | U22(tt, X) | → | activate(X) |
| U31(tt, N) | → | U32(tt, activate(N)) | | U32(tt, N) | → | activate(N) |
| U41(tt, N, XS) | → | U42(tt, activate(N), activate(XS)) | | U42(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) |
| U51(tt, Y) | → | U52(tt, activate(Y)) | | U52(tt, Y) | → | activate(Y) |
| U61(tt, N, X, XS) | → | U62(tt, activate(N), activate(X), activate(XS)) | | U62(tt, N, X, XS) | → | U63(tt, activate(N), activate(X), activate(XS)) |
| U63(tt, N, X, XS) | → | U64(splitAt(activate(N), activate(XS)), activate(X)) | | U64(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) |
| U71(tt, XS) | → | U72(tt, activate(XS)) | | U72(tt, XS) | → | activate(XS) |
| U81(tt, N, XS) | → | U82(tt, activate(N), activate(XS)) | | U82(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) |
| afterNth(N, XS) | → | U11(tt, N, XS) | | fst(pair(X, Y)) | → | U21(tt, X) |
| head(cons(N, XS)) | → | U31(tt, N) | | natsFrom(N) | → | cons(N, n__natsFrom(n__s(N))) |
| sel(N, XS) | → | U41(tt, N, XS) | | snd(pair(X, Y)) | → | U51(tt, Y) |
| splitAt(0, XS) | → | pair(nil, XS) | | splitAt(s(N), cons(X, XS)) | → | U61(tt, N, X, activate(XS)) |
| tail(cons(N, XS)) | → | U71(tt, activate(XS)) | | take(N, XS) | → | U81(tt, N, XS) |
| natsFrom(X) | → | n__natsFrom(X) | | s(X) | → | n__s(X) |
| activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | | activate(n__s(X)) | → | s(activate(X)) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, U64, activate, fst, n__s, U63, U62, U61, U42, U41, head, U21, U22, snd, cons, tail, n__natsFrom, splitAt, U71, U72, 0, s, U51, tt, U82, take, U52, U81, U11, U12, U31, afterNth, U32, sel, nil
Strategy
The following SCCs where found
| splitAt#(s(N), cons(X, XS)) → U61#(tt, N, X, activate(XS)) | U61#(tt, N, X, XS) → U62#(tt, activate(N), activate(X), activate(XS)) |
| U63#(tt, N, X, XS) → splitAt#(activate(N), activate(XS)) | U62#(tt, N, X, XS) → U63#(tt, activate(N), activate(X), activate(XS)) |
| activate#(n__natsFrom(X)) → activate#(X) | activate#(n__s(X)) → activate#(X) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| activate#(n__natsFrom(X)) | → | activate#(X) | | activate#(n__s(X)) | → | activate#(X) |
Rewrite Rules
| U11(tt, N, XS) | → | U12(tt, activate(N), activate(XS)) | | U12(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) |
| U21(tt, X) | → | U22(tt, activate(X)) | | U22(tt, X) | → | activate(X) |
| U31(tt, N) | → | U32(tt, activate(N)) | | U32(tt, N) | → | activate(N) |
| U41(tt, N, XS) | → | U42(tt, activate(N), activate(XS)) | | U42(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) |
| U51(tt, Y) | → | U52(tt, activate(Y)) | | U52(tt, Y) | → | activate(Y) |
| U61(tt, N, X, XS) | → | U62(tt, activate(N), activate(X), activate(XS)) | | U62(tt, N, X, XS) | → | U63(tt, activate(N), activate(X), activate(XS)) |
| U63(tt, N, X, XS) | → | U64(splitAt(activate(N), activate(XS)), activate(X)) | | U64(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) |
| U71(tt, XS) | → | U72(tt, activate(XS)) | | U72(tt, XS) | → | activate(XS) |
| U81(tt, N, XS) | → | U82(tt, activate(N), activate(XS)) | | U82(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) |
| afterNth(N, XS) | → | U11(tt, N, XS) | | fst(pair(X, Y)) | → | U21(tt, X) |
| head(cons(N, XS)) | → | U31(tt, N) | | natsFrom(N) | → | cons(N, n__natsFrom(n__s(N))) |
| sel(N, XS) | → | U41(tt, N, XS) | | snd(pair(X, Y)) | → | U51(tt, Y) |
| splitAt(0, XS) | → | pair(nil, XS) | | splitAt(s(N), cons(X, XS)) | → | U61(tt, N, X, activate(XS)) |
| tail(cons(N, XS)) | → | U71(tt, activate(XS)) | | take(N, XS) | → | U81(tt, N, XS) |
| natsFrom(X) | → | n__natsFrom(X) | | s(X) | → | n__s(X) |
| activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | | activate(n__s(X)) | → | s(activate(X)) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, U64, activate, fst, n__s, U63, U62, U61, U42, U41, head, U21, U22, snd, cons, tail, n__natsFrom, splitAt, U71, U72, 0, s, U51, tt, U82, take, U52, U81, U11, U12, U31, afterNth, U32, sel, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| activate#(n__natsFrom(X)) | → | activate#(X) | | activate#(n__s(X)) | → | activate#(X) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| splitAt#(s(N), cons(X, XS)) | → | U61#(tt, N, X, activate(XS)) | | U61#(tt, N, X, XS) | → | U62#(tt, activate(N), activate(X), activate(XS)) |
| U63#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | | U62#(tt, N, X, XS) | → | U63#(tt, activate(N), activate(X), activate(XS)) |
Rewrite Rules
| U11(tt, N, XS) | → | U12(tt, activate(N), activate(XS)) | | U12(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) |
| U21(tt, X) | → | U22(tt, activate(X)) | | U22(tt, X) | → | activate(X) |
| U31(tt, N) | → | U32(tt, activate(N)) | | U32(tt, N) | → | activate(N) |
| U41(tt, N, XS) | → | U42(tt, activate(N), activate(XS)) | | U42(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) |
| U51(tt, Y) | → | U52(tt, activate(Y)) | | U52(tt, Y) | → | activate(Y) |
| U61(tt, N, X, XS) | → | U62(tt, activate(N), activate(X), activate(XS)) | | U62(tt, N, X, XS) | → | U63(tt, activate(N), activate(X), activate(XS)) |
| U63(tt, N, X, XS) | → | U64(splitAt(activate(N), activate(XS)), activate(X)) | | U64(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) |
| U71(tt, XS) | → | U72(tt, activate(XS)) | | U72(tt, XS) | → | activate(XS) |
| U81(tt, N, XS) | → | U82(tt, activate(N), activate(XS)) | | U82(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) |
| afterNth(N, XS) | → | U11(tt, N, XS) | | fst(pair(X, Y)) | → | U21(tt, X) |
| head(cons(N, XS)) | → | U31(tt, N) | | natsFrom(N) | → | cons(N, n__natsFrom(n__s(N))) |
| sel(N, XS) | → | U41(tt, N, XS) | | snd(pair(X, Y)) | → | U51(tt, Y) |
| splitAt(0, XS) | → | pair(nil, XS) | | splitAt(s(N), cons(X, XS)) | → | U61(tt, N, X, activate(XS)) |
| tail(cons(N, XS)) | → | U71(tt, activate(XS)) | | take(N, XS) | → | U81(tt, N, XS) |
| natsFrom(X) | → | n__natsFrom(X) | | s(X) | → | n__s(X) |
| activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | | activate(n__s(X)) | → | s(activate(X)) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, U64, activate, fst, n__s, U63, U62, U61, U42, U41, head, U21, U22, snd, cons, tail, n__natsFrom, splitAt, U71, U72, 0, s, U51, tt, U82, take, U52, U81, U11, U12, U31, afterNth, U32, sel, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x,y,z): 0
- U12(x,y,z): 0
- U21(x,y): 0
- U22(x,y): 0
- U31(x,y): 0
- U32(x,y): 0
- U41(x,y,z): 0
- U42(x,y,z): 0
- U51(x,y): 0
- U52(x,y): 0
- U61(x1,x2,x3,x4): 0
- U61#(x1,x2,x3,x4): 2x2
- U62(x1,x2,x3,x4): 0
- U62#(x1,x2,x3,x4): 2x2
- U63(x1,x2,x3,x4): 0
- U63#(x1,x2,x3,x4): x2
- U64(x,y): 0
- U71(x,y): 0
- U72(x,y): 0
- U81(x,y,z): 0
- U82(x,y,z): 0
- activate(x): x
- afterNth(x,y): 0
- cons(x,y): 1
- fst(x): 0
- head(x): 0
- n__natsFrom(x): 1
- n__s(x): 3x + 1
- natsFrom(x): 1
- nil: 0
- pair(x,y): 0
- s(x): 3x + 1
- sel(x,y): 0
- snd(x): 0
- splitAt(x,y): 0
- splitAt#(x,y): x
- tail(x): 0
- take(x,y): 0
- tt: 0
Improved Usable rules
| s(X) | → | n__s(X) | | activate(X) | → | X |
| activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | | natsFrom(X) | → | n__natsFrom(X) |
| activate(n__s(X)) | → | s(activate(X)) | | natsFrom(N) | → | cons(N, n__natsFrom(n__s(N))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| splitAt#(s(N), cons(X, XS)) | → | U61#(tt, N, X, activate(XS)) |
Problem 4: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U61#(tt, N, X, XS) | → | U62#(tt, activate(N), activate(X), activate(XS)) | | U63#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) |
| U62#(tt, N, X, XS) | → | U63#(tt, activate(N), activate(X), activate(XS)) |
Rewrite Rules
| U11(tt, N, XS) | → | U12(tt, activate(N), activate(XS)) | | U12(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) |
| U21(tt, X) | → | U22(tt, activate(X)) | | U22(tt, X) | → | activate(X) |
| U31(tt, N) | → | U32(tt, activate(N)) | | U32(tt, N) | → | activate(N) |
| U41(tt, N, XS) | → | U42(tt, activate(N), activate(XS)) | | U42(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) |
| U51(tt, Y) | → | U52(tt, activate(Y)) | | U52(tt, Y) | → | activate(Y) |
| U61(tt, N, X, XS) | → | U62(tt, activate(N), activate(X), activate(XS)) | | U62(tt, N, X, XS) | → | U63(tt, activate(N), activate(X), activate(XS)) |
| U63(tt, N, X, XS) | → | U64(splitAt(activate(N), activate(XS)), activate(X)) | | U64(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) |
| U71(tt, XS) | → | U72(tt, activate(XS)) | | U72(tt, XS) | → | activate(XS) |
| U81(tt, N, XS) | → | U82(tt, activate(N), activate(XS)) | | U82(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) |
| afterNth(N, XS) | → | U11(tt, N, XS) | | fst(pair(X, Y)) | → | U21(tt, X) |
| head(cons(N, XS)) | → | U31(tt, N) | | natsFrom(N) | → | cons(N, n__natsFrom(n__s(N))) |
| sel(N, XS) | → | U41(tt, N, XS) | | snd(pair(X, Y)) | → | U51(tt, Y) |
| splitAt(0, XS) | → | pair(nil, XS) | | splitAt(s(N), cons(X, XS)) | → | U61(tt, N, X, activate(XS)) |
| tail(cons(N, XS)) | → | U71(tt, activate(XS)) | | take(N, XS) | → | U81(tt, N, XS) |
| natsFrom(X) | → | n__natsFrom(X) | | s(X) | → | n__s(X) |
| activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | | activate(n__s(X)) | → | s(activate(X)) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, n__s, fst, activate, U64, U63, U62, U61, U42, U41, head, U21, U22, snd, cons, tail, n__natsFrom, splitAt, U71, U72, 0, s, U51, tt, take, U82, U81, U52, U11, U12, afterNth, U31, U32, sel, nil
Strategy
There are no SCCs!