YES
(VAR YS X XS Y L X1 X2)
(RULES 
active(app(nil,YS)) -> mark(YS)
active(app(cons(X,XS),YS)) -> mark(cons(X,app(XS,YS)))
active(from(X)) -> mark(cons(X,from(s(X))))
active(zWadr(nil,YS)) -> mark(nil)
active(zWadr(XS,nil)) -> mark(nil)
active(zWadr(cons(X,XS),cons(Y,YS))) -> mark(cons(app(Y,cons(X,nil)),zWadr(XS,YS)))
active(prefix(L)) -> mark(cons(nil,zWadr(L,prefix(L))))
active(app(X1,X2)) -> app(active(X1),X2)
active(app(X1,X2)) -> app(X1,active(X2))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(from(X)) -> from(active(X))
active(s(X)) -> s(active(X))
active(zWadr(X1,X2)) -> zWadr(active(X1),X2)
active(zWadr(X1,X2)) -> zWadr(X1,active(X2))
active(prefix(X)) -> prefix(active(X))
app(mark(X1),X2) -> mark(app(X1,X2))
app(X1,mark(X2)) -> mark(app(X1,X2))
cons(mark(X1),X2) -> mark(cons(X1,X2))
from(mark(X)) -> mark(from(X))
s(mark(X)) -> mark(s(X))
zWadr(mark(X1),X2) -> mark(zWadr(X1,X2))
zWadr(X1,mark(X2)) -> mark(zWadr(X1,X2))
prefix(mark(X)) -> mark(prefix(X))
proper(app(X1,X2)) -> app(proper(X1),proper(X2))
proper(nil) -> ok(nil)
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(from(X)) -> from(proper(X))
proper(s(X)) -> s(proper(X))
proper(zWadr(X1,X2)) -> zWadr(proper(X1),proper(X2))
proper(prefix(X)) -> prefix(proper(X))
app(ok(X1),ok(X2)) -> ok(app(X1,X2))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
from(ok(X)) -> ok(from(X))
s(ok(X)) -> ok(s(X))
zWadr(ok(X1),ok(X2)) -> ok(zWadr(X1,X2))
prefix(ok(X)) -> ok(prefix(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
)

Proving termination of rewriting for Ex3_3_25_Bor03_C:

-> Dependency pairs:
nF_active(app(cons(X,XS),YS)) -> nF_cons(X,app(XS,YS))
nF_active(app(cons(X,XS),YS)) -> nF_app(XS,YS)
nF_active(from(X)) -> nF_cons(X,from(s(X)))
nF_active(from(X)) -> nF_from(s(X))
nF_active(from(X)) -> nF_s(X)
nF_active(zWadr(cons(X,XS),cons(Y,YS))) -> nF_cons(app(Y,cons(X,nil)),zWadr(XS,YS))
nF_active(zWadr(cons(X,XS),cons(Y,YS))) -> nF_app(Y,cons(X,nil))
nF_active(zWadr(cons(X,XS),cons(Y,YS))) -> nF_cons(X,nil)
nF_active(zWadr(cons(X,XS),cons(Y,YS))) -> nF_zWadr(XS,YS)
nF_active(prefix(L)) -> nF_cons(nil,zWadr(L,prefix(L)))
nF_active(prefix(L)) -> nF_zWadr(L,prefix(L))
nF_active(prefix(L)) -> nF_prefix(L)
nF_active(app(X1,X2)) -> nF_app(active(X1),X2)
nF_active(app(X1,X2)) -> nF_active(X1)
nF_active(app(X1,X2)) -> nF_app(X1,active(X2))
nF_active(app(X1,X2)) -> nF_active(X2)
nF_active(cons(X1,X2)) -> nF_cons(active(X1),X2)
nF_active(cons(X1,X2)) -> nF_active(X1)
nF_active(from(X)) -> nF_from(active(X))
nF_active(from(X)) -> nF_active(X)
nF_active(s(X)) -> nF_s(active(X))
nF_active(s(X)) -> nF_active(X)
nF_active(zWadr(X1,X2)) -> nF_zWadr(active(X1),X2)
nF_active(zWadr(X1,X2)) -> nF_active(X1)
nF_active(zWadr(X1,X2)) -> nF_zWadr(X1,active(X2))
nF_active(zWadr(X1,X2)) -> nF_active(X2)
nF_active(prefix(X)) -> nF_prefix(active(X))
nF_active(prefix(X)) -> nF_active(X)
nF_app(mark(X1),X2) -> nF_app(X1,X2)
nF_app(X1,mark(X2)) -> nF_app(X1,X2)
nF_cons(mark(X1),X2) -> nF_cons(X1,X2)
nF_from(mark(X)) -> nF_from(X)
nF_s(mark(X)) -> nF_s(X)
nF_zWadr(mark(X1),X2) -> nF_zWadr(X1,X2)
nF_zWadr(X1,mark(X2)) -> nF_zWadr(X1,X2)
nF_prefix(mark(X)) -> nF_prefix(X)
nF_proper(app(X1,X2)) -> nF_app(proper(X1),proper(X2))
nF_proper(app(X1,X2)) -> nF_proper(X1)
nF_proper(app(X1,X2)) -> nF_proper(X2)
nF_proper(cons(X1,X2)) -> nF_cons(proper(X1),proper(X2))
nF_proper(cons(X1,X2)) -> nF_proper(X1)
nF_proper(cons(X1,X2)) -> nF_proper(X2)
nF_proper(from(X)) -> nF_from(proper(X))
nF_proper(from(X)) -> nF_proper(X)
nF_proper(s(X)) -> nF_s(proper(X))
nF_proper(s(X)) -> nF_proper(X)
nF_proper(zWadr(X1,X2)) -> nF_zWadr(proper(X1),proper(X2))
nF_proper(zWadr(X1,X2)) -> nF_proper(X1)
nF_proper(zWadr(X1,X2)) -> nF_proper(X2)
nF_proper(prefix(X)) -> nF_prefix(proper(X))
nF_proper(prefix(X)) -> nF_proper(X)
nF_app(ok(X1),ok(X2)) -> nF_app(X1,X2)
nF_cons(ok(X1),ok(X2)) -> nF_cons(X1,X2)
nF_from(ok(X)) -> nF_from(X)
nF_s(ok(X)) -> nF_s(X)
nF_zWadr(ok(X1),ok(X2)) -> nF_zWadr(X1,X2)
nF_prefix(ok(X)) -> nF_prefix(X)
nF_top(mark(X)) -> nF_top(proper(X))
nF_top(mark(X)) -> nF_proper(X)
nF_top(ok(X)) -> nF_top(active(X))
nF_top(ok(X)) -> nF_active(X)

-> Proof of termination for Ex3_3_25_Bor03_C_1_1:
-> -> Dependency pairs in cycle:
nF_top(mark(X)) -> nF_top(proper(X))
nF_top(ok(X)) -> nF_top(active(X))

UsableRules:
active(app(nil,YS)) -> mark(YS)
active(app(cons(X,XS),YS)) -> mark(cons(X,app(XS,YS)))
active(from(X)) -> mark(cons(X,from(s(X))))
active(zWadr(nil,YS)) -> mark(nil)
active(zWadr(XS,nil)) -> mark(nil)
active(zWadr(cons(X,XS),cons(Y,YS))) -> mark(cons(app(Y,cons(X,nil)),zWadr(XS,YS)))
active(prefix(L)) -> mark(cons(nil,zWadr(L,prefix(L))))
active(app(X1,X2)) -> app(active(X1),X2)
active(app(X1,X2)) -> app(X1,active(X2))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(from(X)) -> from(active(X))
active(s(X)) -> s(active(X))
active(zWadr(X1,X2)) -> zWadr(active(X1),X2)
active(zWadr(X1,X2)) -> zWadr(X1,active(X2))
active(prefix(X)) -> prefix(active(X))
app(mark(X1),X2) -> mark(app(X1,X2))
app(X1,mark(X2)) -> mark(app(X1,X2))
cons(mark(X1),X2) -> mark(cons(X1,X2))
from(mark(X)) -> mark(from(X))
s(mark(X)) -> mark(s(X))
zWadr(mark(X1),X2) -> mark(zWadr(X1,X2))
zWadr(X1,mark(X2)) -> mark(zWadr(X1,X2))
prefix(mark(X)) -> mark(prefix(X))
proper(app(X1,X2)) -> app(proper(X1),proper(X2))
proper(nil) -> ok(nil)
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(from(X)) -> from(proper(X))
proper(s(X)) -> s(proper(X))
proper(zWadr(X1,X2)) -> zWadr(proper(X1),proper(X2))
proper(prefix(X)) -> prefix(proper(X))
app(ok(X1),ok(X2)) -> ok(app(X1,X2))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
from(ok(X)) -> ok(from(X))
s(ok(X)) -> ok(s(X))
zWadr(ok(X1),ok(X2)) -> ok(zWadr(X1,X2))
prefix(ok(X)) -> ok(prefix(X))

Polynomial Interpretation:

[active](X) = X
[app](X1,X2) = X1 + X2 + 1
[nil] = 0
[mark](X) = X + 1
[cons](X1,X2) = X1
[from](X) = X + 1
[s](X) = X
[zWadr](X1,X2) = X1 + X2 + 2
[prefix](X) = X + 1
[proper](X) = X
[ok](X) = X
[top](X) = 0
[nF_top](X) = X

TIME: 1.3238e-2

-> -> Dependency pairs in cycle:
nF_top(ok(X)) -> nF_top(active(X))

UsableRules:
active(app(nil,YS)) -> mark(YS)
active(app(cons(X,XS),YS)) -> mark(cons(X,app(XS,YS)))
active(from(X)) -> mark(cons(X,from(s(X))))
active(zWadr(nil,YS)) -> mark(nil)
active(zWadr(XS,nil)) -> mark(nil)
active(zWadr(cons(X,XS),cons(Y,YS))) -> mark(cons(app(Y,cons(X,nil)),zWadr(XS,YS)))
active(prefix(L)) -> mark(cons(nil,zWadr(L,prefix(L))))
active(app(X1,X2)) -> app(active(X1),X2)
active(app(X1,X2)) -> app(X1,active(X2))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(from(X)) -> from(active(X))
active(s(X)) -> s(active(X))
active(zWadr(X1,X2)) -> zWadr(active(X1),X2)
active(zWadr(X1,X2)) -> zWadr(X1,active(X2))
active(prefix(X)) -> prefix(active(X))
app(mark(X1),X2) -> mark(app(X1,X2))
app(X1,mark(X2)) -> mark(app(X1,X2))
cons(mark(X1),X2) -> mark(cons(X1,X2))
from(mark(X)) -> mark(from(X))
s(mark(X)) -> mark(s(X))
zWadr(mark(X1),X2) -> mark(zWadr(X1,X2))
zWadr(X1,mark(X2)) -> mark(zWadr(X1,X2))
prefix(mark(X)) -> mark(prefix(X))
app(ok(X1),ok(X2)) -> ok(app(X1,X2))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
from(ok(X)) -> ok(from(X))
s(ok(X)) -> ok(s(X))
zWadr(ok(X1),ok(X2)) -> ok(zWadr(X1,X2))
prefix(ok(X)) -> ok(prefix(X))

Polynomial Interpretation:

[active](X) = X
[app](X1,X2) = X1
[nil] = 0
[mark](X) = 0
[cons](X1,X2) = X1
[from](X) = X
[s](X) = X
[zWadr](X1,X2) = X2
[prefix](X) = X
[proper](X) = 0
[ok](X) = X + 1
[top](X) = 0
[nF_top](X) = X

TIME: 4.132e-3


-> Proof of termination for Ex3_3_25_Bor03_C_1_2:
-> -> Dependency pairs in cycle:
nF_proper(app(X1,X2)) -> nF_proper(X1)
nF_proper(prefix(X)) -> nF_proper(X)
nF_proper(zWadr(X1,X2)) -> nF_proper(X2)
nF_proper(zWadr(X1,X2)) -> nF_proper(X1)
nF_proper(s(X)) -> nF_proper(X)
nF_proper(from(X)) -> nF_proper(X)
nF_proper(cons(X1,X2)) -> nF_proper(X2)
nF_proper(cons(X1,X2)) -> nF_proper(X1)
nF_proper(app(X1,X2)) -> nF_proper(X2)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex3_3_25_Bor03_C_1_3:
-> -> Dependency pairs in cycle:
nF_active(app(X1,X2)) -> nF_active(X1)
nF_active(prefix(X)) -> nF_active(X)
nF_active(zWadr(X1,X2)) -> nF_active(X2)
nF_active(zWadr(X1,X2)) -> nF_active(X1)
nF_active(s(X)) -> nF_active(X)
nF_active(from(X)) -> nF_active(X)
nF_active(cons(X1,X2)) -> nF_active(X1)
nF_active(app(X1,X2)) -> nF_active(X2)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex3_3_25_Bor03_C_1_4:
-> -> Dependency pairs in cycle:
nF_prefix(ok(X)) -> nF_prefix(X)
nF_prefix(mark(X)) -> nF_prefix(X)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex3_3_25_Bor03_C_1_5:
-> -> Dependency pairs in cycle:
nF_zWadr(ok(X1),ok(X2)) -> nF_zWadr(X1,X2)
nF_zWadr(X1,mark(X2)) -> nF_zWadr(X1,X2)
nF_zWadr(mark(X1),X2) -> nF_zWadr(X1,X2)

Dependency pairs oriented using subterm criterion.

-> -> Dependency pairs in cycle:
nF_zWadr(X1,mark(X2)) -> nF_zWadr(X1,X2)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex3_3_25_Bor03_C_1_6:
-> -> Dependency pairs in cycle:
nF_s(ok(X)) -> nF_s(X)
nF_s(mark(X)) -> nF_s(X)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex3_3_25_Bor03_C_1_7:
-> -> Dependency pairs in cycle:
nF_from(ok(X)) -> nF_from(X)
nF_from(mark(X)) -> nF_from(X)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex3_3_25_Bor03_C_1_8:
-> -> Dependency pairs in cycle:
nF_app(ok(X1),ok(X2)) -> nF_app(X1,X2)
nF_app(X1,mark(X2)) -> nF_app(X1,X2)
nF_app(mark(X1),X2) -> nF_app(X1,X2)

Dependency pairs oriented using subterm criterion.

-> -> Dependency pairs in cycle:
nF_app(X1,mark(X2)) -> nF_app(X1,X2)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex3_3_25_Bor03_C_1_9:
-> -> Dependency pairs in cycle:
nF_cons(ok(X1),ok(X2)) -> nF_cons(X1,X2)
nF_cons(mark(X1),X2) -> nF_cons(X1,X2)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 2
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.