(VAR N XS YS X ZS)
(STRATEGY CONTEXTSENSITIVE 
  (natsFrom 1)
  (cons 1)
  (s 1)
  (fst 1)
  (pair 1 2)
  (snd 1)
  (splitAt 1 2)
  (0)
  (nil)
  (u 1)
  (head 1)
  (tail 1)
  (sel 1 2)
  (afterNth 1 2)
  (take 1 2)
)
(RULES 
natsFrom(N) -> cons(N,natsFrom(s(N)))
fst(pair(XS,YS)) -> XS
snd(pair(XS,YS)) -> YS
splitAt(0,XS) -> pair(nil,XS)
splitAt(s(N),cons(X,XS)) -> u(splitAt(N,XS),N,X,XS)
u(pair(YS,ZS),N,X,XS) -> pair(cons(X,YS),ZS)
head(cons(N,XS)) -> N
tail(cons(N,XS)) -> XS
sel(N,XS) -> head(afterNth(N,XS))
take(N,XS) -> fst(splitAt(N,XS))
afterNth(N,XS) -> snd(splitAt(N,XS))
)

The TRS is orthogonal, thus termination of innermost context-sensitive rewriting is equivalent to termination of context-sensitive rewriting.

Proving termination of context-sensitive rewriting for ExSec4_2_DLMMU04:

-> Dependency pairs:
nF_splitAt(s(N),cons(X,XS)) -> nF_u(splitAt(N,XS),N,X,XS)
nF_splitAt(s(N),cons(X,XS)) -> nF_splitAt(N,XS)
nF_splitAt(s(N),cons(X,XS)) -> XS
nF_u(pair(YS,ZS),N,X,XS) -> X
nF_tail(cons(N,XS)) -> XS
nF_sel(N,XS) -> nF_head(afterNth(N,XS))
nF_sel(N,XS) -> nF_afterNth(N,XS)
nF_take(N,XS) -> nF_fst(splitAt(N,XS))
nF_take(N,XS) -> nF_splitAt(N,XS)
nF_afterNth(N,XS) -> nF_snd(splitAt(N,XS))
nF_afterNth(N,XS) -> nF_splitAt(N,XS)

-> Proof of termination for ExSec4_2_DLMMU04_1:
-> -> Dependency pairs in cycle:
nF_splitAt(s(N),cons(X,XS)) -> nF_splitAt(N,XS)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in CSDG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.