MAYBE

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

Proof:
 DP Processor:
  DPs:
   app#(app(app(compose(),f),g),x) -> app#(f,x)
   app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
   app#(reverse(),l) -> app#(reverse2(),l)
   app#(reverse(),l) -> app#(app(reverse2(),l),nil())
   app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
   app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
   app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
   last#() -> app#(compose(),hd())
   last#() -> app#(app(compose(),hd()),reverse())
   init#() -> app#(compose(),tl())
   init#() -> app#(app(compose(),tl()),reverse())
   init#() -> app#(compose(),reverse())
   init#() -> app#(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
  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()))
  Usable Rule Processor:
   DPs:
    app#(app(app(compose(),f),g),x) -> app#(f,x)
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
    app#(reverse(),l) -> app#(reverse2(),l)
    app#(reverse(),l) -> app#(app(reverse2(),l),nil())
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    last#() -> app#(compose(),hd())
    last#() -> app#(app(compose(),hd()),reverse())
    init#() -> app#(compose(),tl())
    init#() -> app#(app(compose(),tl()),reverse())
    init#() -> app#(compose(),reverse())
    init#() -> app#(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
   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
   Open