(VAR X Y Z)
(STRATEGY CONTEXTSENSITIVE 
  (primes)
  (sieve 1)
  (from 1)
  (s 1)
  (0)
  (cons 1)
  (head 1)
  (tail 1)
  (if 1)
  (true)
  (false)
  (filter 1 2)
  (divides 1 2)
)
(RULES 
primes -> sieve(from(s(s(0))))
from(X) -> cons(X,from(s(X)))
head(cons(X,Y)) -> X
tail(cons(X,Y)) -> Y
if(true,X,Y) -> X
if(false,X,Y) -> Y
filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y)))
)

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 ExIntrod_GM99:

-> Dependency pairs:
nF_primes -> nF_sieve(from(s(s(0))))
nF_primes -> nF_from(s(s(0)))
nF_tail(cons(X,Y)) -> Y
nF_if(true,X,Y) -> X
nF_if(false,X,Y) -> Y
nF_filter(s(s(X)),cons(Y,Z)) -> nF_if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))

-> Proof of termination for ExIntrod_GM99_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.