YES(?,O(n^1))

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:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {10,9,8}
   transitions:
    app1(19,18) -> 20*
    app1(15,1) -> 16*
    app1(15,3) -> 16*
    app1(15,5) -> 16*
    app1(15,7) -> 16*
    app1(30,17) -> 31*
    app1(20,17) -> 9*
    app1(16,14) -> 8*
    app1(32,31) -> 10*
    app1(19,17) -> 32*
    app1(15,2) -> 16*
    app1(15,4) -> 16*
    app1(15,6) -> 16*
    app1(19,29) -> 30*
    compose1() -> 19*
    reverse1() -> 17*
    tl1() -> 29*
    hd1() -> 18*
    reverse21() -> 15*
    nil1() -> 14*
    app0(3,1) -> 8*
    app0(3,3) -> 8*
    app0(3,5) -> 8*
    app0(3,7) -> 8*
    app0(4,2) -> 8*
    app0(4,4) -> 8*
    app0(4,6) -> 8*
    app0(5,1) -> 8*
    app0(5,3) -> 8*
    app0(5,5) -> 8*
    app0(5,7) -> 8*
    app0(6,2) -> 8*
    app0(1,2) -> 8*
    app0(6,4) -> 8*
    app0(1,4) -> 8*
    app0(6,6) -> 8*
    app0(1,6) -> 8*
    app0(7,1) -> 8*
    app0(2,1) -> 8*
    app0(7,3) -> 8*
    app0(2,3) -> 8*
    app0(7,5) -> 8*
    app0(2,5) -> 8*
    app0(7,7) -> 8*
    app0(2,7) -> 8*
    app0(3,2) -> 8*
    app0(3,4) -> 8*
    app0(3,6) -> 8*
    app0(4,1) -> 8*
    app0(4,3) -> 8*
    app0(4,5) -> 8*
    app0(4,7) -> 8*
    app0(5,2) -> 8*
    app0(5,4) -> 8*
    app0(5,6) -> 8*
    app0(6,1) -> 8*
    app0(1,1) -> 8*
    app0(6,3) -> 8*
    app0(1,3) -> 8*
    app0(6,5) -> 8*
    app0(1,5) -> 8*
    app0(6,7) -> 8*
    app0(1,7) -> 8*
    app0(7,2) -> 8*
    app0(2,2) -> 8*
    app0(7,4) -> 8*
    app0(2,4) -> 8*
    app0(7,6) -> 8*
    app0(2,6) -> 8*
    compose0() -> 1*
    reverse0() -> 2*
    reverse20() -> 3*
    nil0() -> 4*
    cons0() -> 5*
    hd0() -> 6*
    tl0() -> 7*
    last0() -> 9*
    init0() -> 10*
    14 -> 8*
  problem:
   
  Qed