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 = 1
  reverse_A = 4
  reverse#_A = 4
  reverse2_A = 1
  reverse2#_A = 1
  nil_A = 1
  nil#_A = 1
  cons_A = 2
  cons#_A = 2
  hd_A = 1
  hd#_A = 1
  tl_A = 1
  tl#_A = 1
  last_A = 9
  last#_A = 9
  init_A = 16
  init#_A = 16

precedence:

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