(VAR X)
(STRATEGY CONTEXTSENSITIVE 
  (from 1)
  (cons 1)
  (s 1)
)
(RULES 
from(X) -> cons(X,from(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 Ex3_3_25_Bor03_1:

-> Dependency pairs:
No dependency pairs found.

-> Proof of termination for Ex3_3_25_Bor03_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 XS YS Y L)
(STRATEGY CONTEXTSENSITIVE 
  (app 1 2)
  (cons 1)
  (nil)
  (zWadr 1 2)
  (prefix 1)
)
(RULES 
app(cons(X,XS),YS) -> cons(X,app(XS,YS))
app(nil,YS) -> YS
zWadr(cons(X,XS),cons(Y,YS)) -> cons(app(Y,cons(X,nil)),zWadr(XS,YS))
zWadr(XS,nil) -> nil
zWadr(nil,YS) -> nil
prefix(L) -> cons(nil,zWadr(L,prefix(L)))
)

Proving termination of context-sensitive rewriting for Ex3_3_25_Bor03_2:

-> Dependency pairs:
nF_zWadr(cons(X,XS),cons(Y,YS)) -> nF_app(Y,cons(X,nil))

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