(VAR X Y) (STRATEGY CONTEXTSENSITIVE (eq) (false) (s) (0) (true) ) (RULES eq(X,Y) -> false eq(s(X),s(Y)) -> eq(X,Y) eq(0,0) -> true ) Proving termination of context-sensitive rewriting for Ex1_GL02a_1: -> Dependency pairs: nF_eq(s(X),s(Y)) -> nF_eq(X,Y) -> Proof of termination for Ex1_GL02a_1: -> -> Dependency pairs in cycle: nF_eq(s(X),s(Y)) -> nF_eq(X,Y) Polynomial Interpretation: [s](X) = X + 1 TIME: 1.488299999999998e-2 Termination proved: There exists a projection such that there are no minimal mu-rewrite sequences in cycle. 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) (STRATEGY CONTEXTSENSITIVE (inf 1) (cons) (s) ) (RULES inf(X) -> cons(X,inf(s(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_GL02a_2: -> Dependency pairs: No dependency pairs found. -> Proof of termination for Ex1_GL02a_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 (VAR X Y L) (STRATEGY CONTEXTSENSITIVE (take 1 2) (s) (cons) (0) (nil) ) (RULES take(s(X),cons(Y,L)) -> cons(Y,take(X,L)) take(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 Ex1_GL02a_3: -> Dependency pairs: No dependency pairs found. -> Proof of termination for Ex1_GL02a_3: 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 L) (STRATEGY CONTEXTSENSITIVE (length 1) (cons) (s) (nil) (0) ) (RULES length(cons(X,L)) -> s(length(L)) length(nil) -> 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 Ex1_GL02a_4: -> Dependency pairs: No dependency pairs found. -> Proof of termination for Ex1_GL02a_4: 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.