YES
(VAR a x k d)
(RULES 
f(a,empty) -> g(a,empty)
f(a,cons(x,k)) -> f(cons(x,a),k)
g(empty,d) -> d
g(cons(x,k),d) -> g(k,cons(x,d))
)

The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting.

Proving termination of innermost rewriting for jones6:

-> Dependency pairs:
nF_f(a,empty) -> nF_g(a,empty)
nF_f(a,cons(x,k)) -> nF_f(cons(x,a),k)
nF_g(cons(x,k),d) -> nF_g(k,cons(x,d))

-> Proof of termination for jones6_1_1:
-> -> Dependency pairs in cycle:
nF_f(a,cons(x,k)) -> nF_f(cons(x,a),k)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for jones6_1_2:
-> -> Dependency pairs in cycle:
nF_g(cons(x,k),d) -> nF_g(k,cons(x,d))

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.