YES

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:
 Uncurry Processor:
  compose3(f,g,x) -> app(g,app(f,x))
  reverse1(l) -> reverse22(l,nil())
  reverse22(nil(),l) -> l
  reverse22(cons2(x,xs),l) -> reverse22(xs,cons2(x,l))
  hd1(cons2(x,xs)) -> x
  tl1(cons2(x,xs)) -> xs
  last() -> compose2(hd(),reverse())
  init() -> compose2(reverse(),compose2(tl(),reverse()))
  app(compose2(x6,x5),x7) -> compose3(x6,x5,x7)
  app(compose1(x6),x7) -> compose2(x6,x7)
  app(compose(),x7) -> compose1(x7)
  app(reverse(),x7) -> reverse1(x7)
  app(reverse21(x6),x7) -> reverse22(x6,x7)
  app(reverse2(),x7) -> reverse21(x7)
  app(cons1(x6),x7) -> cons2(x6,x7)
  app(cons(),x7) -> cons1(x7)
  app(hd(),x7) -> hd1(x7)
  app(tl(),x7) -> tl1(x7)
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [tl1](x0) = x0 + 2,
    
    [hd1](x0) = x0 + 5,
    
    [cons2](x0, x1) = x0 + x1 + 1,
    
    [cons1](x0) = x0 + 4,
    
    [reverse22](x0, x1) = x0 + x1 + 2,
    
    [reverse21](x0) = x0 + 6,
    
    [reverse1](x0) = x0 + 2,
    
    [compose1](x0) = x0,
    
    [compose3](x0, x1, x2) = 2x0 + 2x1 + x2,
    
    [compose2](x0, x1) = x0 + x1,
    
    [init] = 3,
    
    [last] = 5,
    
    [tl] = 1,
    
    [hd] = 4,
    
    [cons] = 4,
    
    [nil] = 0,
    
    [reverse2] = 3,
    
    [reverse] = 1,
    
    [app](x0, x1) = 2x0 + x1,
    
    [compose] = 0
   orientation:
    compose3(f,g,x) = 2f + 2g + x >= 2f + 2g + x = app(g,app(f,x))
    
    reverse1(l) = l + 2 >= l + 2 = reverse22(l,nil())
    
    reverse22(nil(),l) = l + 2 >= l = l
    
    reverse22(cons2(x,xs),l) = l + x + xs + 3 >= l + x + xs + 3 = reverse22(xs,cons2(x,l))
    
    hd1(cons2(x,xs)) = x + xs + 6 >= x = x
    
    tl1(cons2(x,xs)) = x + xs + 3 >= xs = xs
    
    last() = 5 >= 5 = compose2(hd(),reverse())
    
    init() = 3 >= 3 = compose2(reverse(),compose2(tl(),reverse()))
    
    app(compose2(x6,x5),x7) = 2x5 + 2x6 + x7 >= 2x5 + 2x6 + x7 = compose3(x6,x5,x7)
    
    app(compose1(x6),x7) = 2x6 + x7 >= x6 + x7 = compose2(x6,x7)
    
    app(compose(),x7) = x7 >= x7 = compose1(x7)
    
    app(reverse(),x7) = x7 + 2 >= x7 + 2 = reverse1(x7)
    
    app(reverse21(x6),x7) = 2x6 + x7 + 12 >= x6 + x7 + 2 = reverse22(x6,x7)
    
    app(reverse2(),x7) = x7 + 6 >= x7 + 6 = reverse21(x7)
    
    app(cons1(x6),x7) = 2x6 + x7 + 8 >= x6 + x7 + 1 = cons2(x6,x7)
    
    app(cons(),x7) = x7 + 8 >= x7 + 4 = cons1(x7)
    
    app(hd(),x7) = x7 + 8 >= x7 + 5 = hd1(x7)
    
    app(tl(),x7) = x7 + 2 >= x7 + 2 = tl1(x7)
   problem:
    compose3(f,g,x) -> app(g,app(f,x))
    reverse1(l) -> reverse22(l,nil())
    reverse22(cons2(x,xs),l) -> reverse22(xs,cons2(x,l))
    last() -> compose2(hd(),reverse())
    init() -> compose2(reverse(),compose2(tl(),reverse()))
    app(compose2(x6,x5),x7) -> compose3(x6,x5,x7)
    app(compose1(x6),x7) -> compose2(x6,x7)
    app(compose(),x7) -> compose1(x7)
    app(reverse(),x7) -> reverse1(x7)
    app(reverse2(),x7) -> reverse21(x7)
    app(tl(),x7) -> tl1(x7)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [tl1](x0) = x0,
     
     [cons2](x0, x1) = 4x0 + x1 + 5,
     
     [reverse22](x0, x1) = x0 + x1,
     
     [reverse21](x0) = x0 + 4,
     
     [reverse1](x0) = x0,
     
     [compose1](x0) = x0,
     
     [compose3](x0, x1, x2) = x0 + x1 + x2,
     
     [compose2](x0, x1) = x0 + x1,
     
     [init] = 6,
     
     [last] = 4,
     
     [tl] = 6,
     
     [hd] = 4,
     
     [nil] = 0,
     
     [reverse2] = 4,
     
     [reverse] = 0,
     
     [app](x0, x1) = x0 + x1,
     
     [compose] = 0
    orientation:
     compose3(f,g,x) = f + g + x >= f + g + x = app(g,app(f,x))
     
     reverse1(l) = l >= l = reverse22(l,nil())
     
     reverse22(cons2(x,xs),l) = l + 4x + xs + 5 >= l + 4x + xs + 5 = reverse22(xs,cons2(x,l))
     
     last() = 4 >= 4 = compose2(hd(),reverse())
     
     init() = 6 >= 6 = compose2(reverse(),compose2(tl(),reverse()))
     
     app(compose2(x6,x5),x7) = x5 + x6 + x7 >= x5 + x6 + x7 = compose3(x6,x5,x7)
     
     app(compose1(x6),x7) = x6 + x7 >= x6 + x7 = compose2(x6,x7)
     
     app(compose(),x7) = x7 >= x7 = compose1(x7)
     
     app(reverse(),x7) = x7 >= x7 = reverse1(x7)
     
     app(reverse2(),x7) = x7 + 4 >= x7 + 4 = reverse21(x7)
     
     app(tl(),x7) = x7 + 6 >= x7 = tl1(x7)
    problem:
     compose3(f,g,x) -> app(g,app(f,x))
     reverse1(l) -> reverse22(l,nil())
     reverse22(cons2(x,xs),l) -> reverse22(xs,cons2(x,l))
     last() -> compose2(hd(),reverse())
     init() -> compose2(reverse(),compose2(tl(),reverse()))
     app(compose2(x6,x5),x7) -> compose3(x6,x5,x7)
     app(compose1(x6),x7) -> compose2(x6,x7)
     app(compose(),x7) -> compose1(x7)
     app(reverse(),x7) -> reverse1(x7)
     app(reverse2(),x7) -> reverse21(x7)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [cons2](x0, x1) = 4x0 + x1,
      
      [reverse22](x0, x1) = x0 + x1,
      
      [reverse21](x0) = x0,
      
      [reverse1](x0) = x0,
      
      [compose1](x0) = x0,
      
      [compose3](x0, x1, x2) = x0 + x1 + x2,
      
      [compose2](x0, x1) = x0 + x1,
      
      [init] = 0,
      
      [last] = 0,
      
      [tl] = 0,
      
      [hd] = 0,
      
      [nil] = 0,
      
      [reverse2] = 1,
      
      [reverse] = 0,
      
      [app](x0, x1) = x0 + x1,
      
      [compose] = 0
     orientation:
      compose3(f,g,x) = f + g + x >= f + g + x = app(g,app(f,x))
      
      reverse1(l) = l >= l = reverse22(l,nil())
      
      reverse22(cons2(x,xs),l) = l + 4x + xs >= l + 4x + xs = reverse22(xs,cons2(x,l))
      
      last() = 0 >= 0 = compose2(hd(),reverse())
      
      init() = 0 >= 0 = compose2(reverse(),compose2(tl(),reverse()))
      
      app(compose2(x6,x5),x7) = x5 + x6 + x7 >= x5 + x6 + x7 = compose3(x6,x5,x7)
      
      app(compose1(x6),x7) = x6 + x7 >= x6 + x7 = compose2(x6,x7)
      
      app(compose(),x7) = x7 >= x7 = compose1(x7)
      
      app(reverse(),x7) = x7 >= x7 = reverse1(x7)
      
      app(reverse2(),x7) = x7 + 1 >= x7 = reverse21(x7)
     problem:
      compose3(f,g,x) -> app(g,app(f,x))
      reverse1(l) -> reverse22(l,nil())
      reverse22(cons2(x,xs),l) -> reverse22(xs,cons2(x,l))
      last() -> compose2(hd(),reverse())
      init() -> compose2(reverse(),compose2(tl(),reverse()))
      app(compose2(x6,x5),x7) -> compose3(x6,x5,x7)
      app(compose1(x6),x7) -> compose2(x6,x7)
      app(compose(),x7) -> compose1(x7)
      app(reverse(),x7) -> reverse1(x7)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [cons2](x0, x1) = 2x0 + x1 + 4,
       
       [reverse22](x0, x1) = x0 + x1,
       
       [reverse1](x0) = x0,
       
       [compose1](x0) = x0,
       
       [compose3](x0, x1, x2) = 4x0 + 4x1 + x2,
       
       [compose2](x0, x1) = 4x0 + x1,
       
       [init] = 0,
       
       [last] = 0,
       
       [tl] = 0,
       
       [hd] = 0,
       
       [nil] = 0,
       
       [reverse] = 0,
       
       [app](x0, x1) = 4x0 + x1,
       
       [compose] = 5
      orientation:
       compose3(f,g,x) = 4f + 4g + x >= 4f + 4g + x = app(g,app(f,x))
       
       reverse1(l) = l >= l = reverse22(l,nil())
       
       reverse22(cons2(x,xs),l) = l + 2x + xs + 4 >= l + 2x + xs + 4 = reverse22(xs,cons2(x,l))
       
       last() = 0 >= 0 = compose2(hd(),reverse())
       
       init() = 0 >= 0 = compose2(reverse(),compose2(tl(),reverse()))
       
       app(compose2(x6,x5),x7) = 4x5 + 16x6 + x7 >= 4x5 + 4x6 + x7 = compose3(x6,x5,x7)
       
       app(compose1(x6),x7) = 4x6 + x7 >= 4x6 + x7 = compose2(x6,x7)
       
       app(compose(),x7) = x7 + 20 >= x7 = compose1(x7)
       
       app(reverse(),x7) = x7 >= x7 = reverse1(x7)
      problem:
       compose3(f,g,x) -> app(g,app(f,x))
       reverse1(l) -> reverse22(l,nil())
       reverse22(cons2(x,xs),l) -> reverse22(xs,cons2(x,l))
       last() -> compose2(hd(),reverse())
       init() -> compose2(reverse(),compose2(tl(),reverse()))
       app(compose2(x6,x5),x7) -> compose3(x6,x5,x7)
       app(compose1(x6),x7) -> compose2(x6,x7)
       app(reverse(),x7) -> reverse1(x7)
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [cons2](x0, x1) = x0 + x1,
        
        [reverse22](x0, x1) = x0 + x1,
        
        [reverse1](x0) = x0 + 2,
        
        [compose1](x0) = 4x0 + 4,
        
        [compose3](x0, x1, x2) = x0 + x1 + x2 + 4,
        
        [compose2](x0, x1) = 4x0 + x1 + 2,
        
        [init] = 4,
        
        [last] = 2,
        
        [tl] = 0,
        
        [hd] = 0,
        
        [nil] = 1,
        
        [reverse] = 0,
        
        [app](x0, x1) = x0 + x1 + 2
       orientation:
        compose3(f,g,x) = f + g + x + 4 >= f + g + x + 4 = app(g,app(f,x))
        
        reverse1(l) = l + 2 >= l + 1 = reverse22(l,nil())
        
        reverse22(cons2(x,xs),l) = l + x + xs >= l + x + xs = reverse22(xs,cons2(x,l))
        
        last() = 2 >= 2 = compose2(hd(),reverse())
        
        init() = 4 >= 4 = compose2(reverse(),compose2(tl(),reverse()))
        
        app(compose2(x6,x5),x7) = x5 + 4x6 + x7 + 4 >= x5 + x6 + x7 + 4 = compose3(x6,x5,x7)
        
        app(compose1(x6),x7) = 4x6 + x7 + 6 >= 4x6 + x7 + 2 = compose2(x6,x7)
        
        app(reverse(),x7) = x7 + 2 >= x7 + 2 = reverse1(x7)
       problem:
        compose3(f,g,x) -> app(g,app(f,x))
        reverse22(cons2(x,xs),l) -> reverse22(xs,cons2(x,l))
        last() -> compose2(hd(),reverse())
        init() -> compose2(reverse(),compose2(tl(),reverse()))
        app(compose2(x6,x5),x7) -> compose3(x6,x5,x7)
        app(reverse(),x7) -> reverse1(x7)
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [cons2](x0, x1) = 4x0 + x1,
         
         [reverse22](x0, x1) = 2x0 + 2x1 + 1,
         
         [reverse1](x0) = x0,
         
         [compose3](x0, x1, x2) = 4x0 + 4x1 + x2 + 2,
         
         [compose2](x0, x1) = 4x0 + 2x1 + 2,
         
         [init] = 6,
         
         [last] = 6,
         
         [tl] = 0,
         
         [hd] = 1,
         
         [reverse] = 0,
         
         [app](x0, x1) = 4x0 + x1
        orientation:
         compose3(f,g,x) = 4f + 4g + x + 2 >= 4f + 4g + x = app(g,app(f,x))
         
         reverse22(cons2(x,xs),l) = 2l + 8x + 2xs + 1 >= 2l + 8x + 2xs + 1 = reverse22(xs,cons2(x,l))
         
         last() = 6 >= 6 = compose2(hd(),reverse())
         
         init() = 6 >= 6 = compose2(reverse(),compose2(tl(),reverse()))
         
         app(compose2(x6,x5),x7) = 8x5 + 16x6 + x7 + 8 >= 4x5 + 4x6 + x7 + 2 = compose3(x6,x5,x7)
         
         app(reverse(),x7) = x7 >= x7 = reverse1(x7)
        problem:
         reverse22(cons2(x,xs),l) -> reverse22(xs,cons2(x,l))
         last() -> compose2(hd(),reverse())
         init() -> compose2(reverse(),compose2(tl(),reverse()))
         app(reverse(),x7) -> reverse1(x7)
        DP Processor:
         DPs:
          reverse2{2,#}(cons2(x,xs),l) -> reverse2{2,#}(xs,cons2(x,l))
         TRS:
          reverse22(cons2(x,xs),l) -> reverse22(xs,cons2(x,l))
          last() -> compose2(hd(),reverse())
          init() -> compose2(reverse(),compose2(tl(),reverse()))
          app(reverse(),x7) -> reverse1(x7)
         Subterm Criterion Processor:
          simple projection:
           pi(reverse2{2,#}) = 0
          problem:
           DPs:
            
           TRS:
            reverse22(cons2(x,xs),l) -> reverse22(xs,cons2(x,l))
            last() -> compose2(hd(),reverse())
            init() -> compose2(reverse(),compose2(tl(),reverse()))
            app(reverse(),x7) -> reverse1(x7)
          Qed