(VAR X) (STRATEGY CONTEXTSENSITIVE (f 3) (a) (b) ) (RULES f(a,b,X) -> f(X,X,X) ) 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 Ex1_GM99_1: -> Dependency pairs: nF_f(a,b,X) -> nF_f(X,X,X) -> Proof of termination for Ex1_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 (VAR ) (STRATEGY CONTEXTSENSITIVE (c) (b) (a) ) (RULES c -> b c -> a ) Proving termination of context-sensitive rewriting for Ex1_GM99_2: -> Dependency pairs: No dependency pairs found. -> Proof of termination for Ex1_GM99_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.