YES
(VAR k l x y)
(RULES 
app(nil,k) -> k
app(l,nil) -> l
app(cons(x,l),k) -> cons(x,app(l,k))
sum(cons(x,nil)) -> cons(x,nil)
sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
plus(0,y) -> y
plus(s(x),y) -> s(plus(x,y))
)

Proving termination of rewriting for _3_17:

-> Dependency pairs:
nF_app(cons(x,l),k) -> nF_app(l,k)
nF_sum(cons(x,cons(y,l))) -> nF_sum(cons(plus(x,y),l))
nF_sum(cons(x,cons(y,l))) -> nF_plus(x,y)
nF_sum(app(l,cons(x,cons(y,k)))) -> nF_sum(app(l,sum(cons(x,cons(y,k)))))
nF_sum(app(l,cons(x,cons(y,k)))) -> nF_app(l,sum(cons(x,cons(y,k))))
nF_sum(app(l,cons(x,cons(y,k)))) -> nF_sum(cons(x,cons(y,k)))
nF_plus(s(x),y) -> nF_plus(x,y)

-> Proof of termination for _3_17_1_1:
-> -> Dependency pairs in cycle:
nF_sum(app(l,cons(x,cons(y,k)))) -> nF_sum(app(l,sum(cons(x,cons(y,k)))))

UsableRules:
app(nil,k) -> k
app(l,nil) -> l
app(cons(x,l),k) -> cons(x,app(l,k))
sum(cons(x,nil)) -> cons(x,nil)
sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
plus(0,y) -> y
plus(s(x),y) -> s(plus(x,y))

Polynomial Interpretation:

[app](X1,X2) = X1 + X2
[nil] = 0
[cons](X1,X2) = X2 + 1
[sum](X) = 1
[plus](X1,X2) = X2
[0] = 0
[s](X) = 0
[nF_sum](X) = X

TIME: 4.1497e-2


-> Proof of termination for _3_17_1_2:
-> -> Dependency pairs in cycle:
nF_sum(cons(x,cons(y,l))) -> nF_sum(cons(plus(x,y),l))

UsableRules:
plus(0,y) -> y
plus(s(x),y) -> s(plus(x,y))

Polynomial Interpretation:

[app](X1,X2) = 0
[nil] = 0
[cons](X1,X2) = X2 + 1
[sum](X) = 0
[plus](X1,X2) = X2
[0] = 0
[s](X) = 0
[nF_sum](X) = X

TIME: 3.9837e-2


-> Proof of termination for _3_17_1_3:
-> -> Dependency pairs in cycle:
nF_plus(s(x),y) -> nF_plus(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for _3_17_1_4:
-> -> Dependency pairs in cycle:
nF_app(cons(x,l),k) -> nF_app(l,k)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + 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.