(VAR N X Y) (STRATEGY CONTEXTSENSITIVE (terms 1) (cons 1) (recip 1) (sqr 1) (s) (add 1 2) (dbl 1) (0) ) (RULES terms(N) -> cons(recip(sqr(N)),terms(s(N))) sqr(s(X)) -> s(add(sqr(X),dbl(X))) sqr(0) -> 0 add(s(X),Y) -> s(add(X,Y)) add(0,X) -> X dbl(s(X)) -> s(s(dbl(X))) dbl(0) -> 0 ) 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 Ex26_Luc03b_1: -> Dependency pairs: nF_terms(N) -> nF_sqr(N) -> Proof of termination for Ex26_Luc03b_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 (VAR X Y Z) (STRATEGY CONTEXTSENSITIVE (first 1 2) (s) (cons 1) (0) (nil) ) (RULES first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) first(0,X) -> nil ) 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 Ex26_Luc03b_2: -> Dependency pairs: No dependency pairs found. -> Proof of termination for Ex26_Luc03b_2: 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.