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 + 1
  app#_A(x1,x2) = x1 + x2 + 1
  compose_A = 1
  compose#_A = 0
  reverse_A = 6
  reverse#_A = 1
  reverse2_A = 3
  reverse2#_A = 0
  nil_A = 1
  nil#_A = 0
  cons_A = 1
  cons#_A = 1
  hd_A = 1
  hd#_A = 0
  tl_A = 1
  tl#_A = 0
  last_A = 10
  last#_A = 11
  init_A = 19
  init#_A = 20

precedence:

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