YES

TRS:

  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()))

linear polynomial interpretations on N:

  app_A(x1,x2) = x1 + x2
  app#_A(x1,x2) = x1 + x2
  compose_A = 1
  compose#_A = 1
  reverse_A = 1
  reverse#_A = 1
  reverse2_A = 0
  reverse2#_A = 0
  nil_A = 0
  nil#_A = 0
  cons_A = 0
  cons#_A = 0
  hd_A = 0
  hd#_A = 0
  tl_A = 0
  tl#_A = 0
  last_A = 3
  last#_A = 3
  init_A = 5
  init#_A = 5

precedence:

  nil = last = init > app = tl > compose = reverse = cons = hd > reverse2