(VAR X XS N Y YS)
(STRATEGY CONTEXTSENSITIVE 
  (pairNs)
  (cons 1)
  (0)
  (incr 1)
  (oddNs)
  (s 1)
  (take 1 2)
  (nil)
  (zip 1 2)
  (pair 1 2)
  (tail 1)
  (repItems 1)
)
(RULES 
pairNs -> cons(0,incr(oddNs))
oddNs -> incr(pairNs)
incr(cons(X,XS)) -> cons(s(X),incr(XS))
take(0,XS) -> nil
take(s(N),cons(X,XS)) -> cons(X,take(N,XS))
zip(nil,XS) -> nil
zip(X,nil) -> nil
zip(cons(X,XS),cons(Y,YS)) -> cons(pair(X,Y),zip(XS,YS))
tail(cons(X,XS)) -> XS
repItems(nil) -> nil
repItems(cons(X,XS)) -> cons(X,cons(X,repItems(XS)))
)

Proving termination of context-sensitive rewriting for Ex5_DLMMU04:

-> Dependency pairs:
nF_oddNs -> nF_incr(pairNs)
nF_oddNs -> nF_pairNs
nF_tail(cons(X,XS)) -> XS

-> Proof of termination for Ex5_DLMMU04_1:
Termination proved: No cycles in dependency graph.

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.