(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.