YES
(VAR f g x l xs)
(RULES 
app(app(app(compose,f),g),x) -> app(g,app(f,x))
app(reverse,l) -> app(app(reverse2,l),nil)
app(app(reverse2,nil),l) -> l
app(app(reverse2,app(app(cons,x),xs)),l) -> app(app(reverse2,xs),app(app(cons,x),l))
app(hd,app(app(cons,x),xs)) -> x
app(tl,app(app(cons,x),xs)) -> xs
last -> app(app(compose,hd),reverse)
init -> app(app(compose,reverse),app(app(compose,tl),reverse))
)

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 ReverseLastInit:

-> Dependency pairs:
nF_app(app(app(compose,f),g),x) -> nF_app(g,app(f,x))
nF_app(app(app(compose,f),g),x) -> nF_app(f,x)
nF_app(reverse,l) -> nF_app(app(reverse2,l),nil)
nF_app(reverse,l) -> nF_app(reverse2,l)
nF_app(app(reverse2,app(app(cons,x),xs)),l) -> nF_app(app(reverse2,xs),app(app(cons,x),l))
nF_app(app(reverse2,app(app(cons,x),xs)),l) -> nF_app(reverse2,xs)
nF_app(app(reverse2,app(app(cons,x),xs)),l) -> nF_app(app(cons,x),l)
nF_app(app(reverse2,app(app(cons,x),xs)),l) -> nF_app(cons,x)
nF_last -> nF_app(app(compose,hd),reverse)
nF_last -> nF_app(compose,hd)
nF_init -> nF_app(app(compose,reverse),app(app(compose,tl),reverse))
nF_init -> nF_app(compose,reverse)
nF_init -> nF_app(app(compose,tl),reverse)
nF_init -> nF_app(compose,tl)

-> Dependency pairs narrowed: 
nF_app(app(reverse2,app(app(cons,x),xs)),l) -> nF_app(app(cons,x),l)

-> New dependency pairs: 
There are no new dependency pairs.

-> Proof of termination for ReverseLastInit_1:
-> -> Dependency pairs in cycle:
nF_app(app(app(compose,f),g),x) -> nF_app(g,app(f,x))
nF_app(app(reverse2,app(app(cons,x),xs)),l) -> nF_app(app(reverse2,xs),app(app(cons,x),l))
nF_app(reverse,l) -> nF_app(app(reverse2,l),nil)
nF_app(app(app(compose,f),g),x) -> nF_app(f,x)

UsableRules:
app(app(app(compose,f),g),x) -> app(g,app(f,x))
app(reverse,l) -> app(app(reverse2,l),nil)
app(app(reverse2,nil),l) -> l
app(app(reverse2,app(app(cons,x),xs)),l) -> app(app(reverse2,xs),app(app(cons,x),l))
app(hd,app(app(cons,x),xs)) -> x
app(tl,app(app(cons,x),xs)) -> xs

Polynomial Interpretation:

[app](X1,X2) = X1 + X2 + 1
[compose] = 0
[reverse] = 1
[reverse2] = 0
[nil] = 0
[cons] = 1
[hd] = 0
[tl] = 0
[last] = 0
[init] = 0
[nF_app](X1,X2) = X1 + X2

TIME: 4.8518e-2

-> -> Dependency pairs in cycle:
nF_app(app(app(compose,f),g),x) -> nF_app(g,app(f,x))
nF_app(reverse,l) -> nF_app(app(reverse2,l),nil)
nF_app(app(reverse2,app(app(cons,x),xs)),l) -> nF_app(app(reverse2,xs),app(app(cons,x),l))

UsableRules:
app(app(app(compose,f),g),x) -> app(g,app(f,x))
app(reverse,l) -> app(app(reverse2,l),nil)
app(app(reverse2,nil),l) -> l
app(app(reverse2,app(app(cons,x),xs)),l) -> app(app(reverse2,xs),app(app(cons,x),l))
app(hd,app(app(cons,x),xs)) -> x
app(tl,app(app(cons,x),xs)) -> xs

Polynomial Interpretation:

[app](X1,X2) = X1 + X2
[compose] = 1
[reverse] = 1
[reverse2] = 0
[nil] = 0
[cons] = 1
[hd] = 0
[tl] = 0
[last] = 0
[init] = 0
[nF_app](X1,X2) = X1 + X2

TIME: 4.8521e-2

-> -> Dependency pairs in cycle:
nF_app(app(app(compose,f),g),x) -> nF_app(g,app(f,x))
nF_app(app(reverse2,app(app(cons,x),xs)),l) -> nF_app(app(reverse2,xs),app(app(cons,x),l))

UsableRules:
app(app(app(compose,f),g),x) -> app(g,app(f,x))
app(reverse,l) -> app(app(reverse2,l),nil)
app(app(reverse2,nil),l) -> l
app(app(reverse2,app(app(cons,x),xs)),l) -> app(app(reverse2,xs),app(app(cons,x),l))
app(hd,app(app(cons,x),xs)) -> x
app(tl,app(app(cons,x),xs)) -> xs

Polynomial Interpretation:

[app](X1,X2) = X1 + X2 + 1
[compose] = 0
[reverse] = 1
[reverse2] = 0
[nil] = 0
[cons] = 0
[hd] = 0
[tl] = 0
[last] = 0
[init] = 0
[nF_app](X1,X2) = X1

TIME: 4.6042e-2

-> -> Dependency pairs in cycle:
nF_app(app(app(compose,f),g),x) -> nF_app(g,app(f,x))

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.