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:
 Extended Uncurrying Processor:
  application symbol: app
  symbol table:
   init ==> init0/0
   last ==> last0/0
   tl ==> tl0/0 tl1/1
   hd ==> hd0/0 hd1/1
   cons ==> cons0/0 cons1/1 cons2/2
   nil ==> nil0/0
   reverse2 ==> reverse20/0 reverse21/1 reverse22/2
   reverse ==> reverse0/0 reverse1/1
   compose ==> compose0/0 compose1/1 compose2/2 compose3/3
   
  uncurry-rules:
   app(compose2(x5,x6),x7) -> compose3(x5,x6,x7)
   app(compose1(x5),x6) -> compose2(x5,x6)
   app(compose0(),x5) -> compose1(x5)
   app(reverse0(),x9) -> reverse1(x9)
   app(reverse21(x11),x12) -> reverse22(x11,x12)
   app(reverse20(),x11) -> reverse21(x11)
   app(cons1(x15),x16) -> cons2(x15,x16)
   app(cons0(),x15) -> cons1(x15)
   app(hd0(),x18) -> hd1(x18)
   app(tl0(),x20) -> tl1(x20)
  eta-rules:
   
  problem:
   compose3(f,g,x) -> app(g,app(f,x))
   reverse1(l) -> reverse22(l,nil0())
   reverse22(nil0(),l) -> l
   reverse22(cons2(x,xs),l) -> reverse22(xs,cons2(x,l))
   hd1(cons2(x,xs)) -> x
   tl1(cons2(x,xs)) -> xs
   last0() -> compose2(hd0(),reverse0())
   init0() -> compose2(reverse0(),compose2(tl0(),reverse0()))
   app(compose2(x5,x6),x7) -> compose3(x5,x6,x7)
   app(compose1(x5),x6) -> compose2(x5,x6)
   app(compose0(),x5) -> compose1(x5)
   app(reverse0(),x9) -> reverse1(x9)
   app(reverse21(x11),x12) -> reverse22(x11,x12)
   app(reverse20(),x11) -> reverse21(x11)
   app(cons1(x15),x16) -> cons2(x15,x16)
   app(cons0(),x15) -> cons1(x15)
   app(hd0(),x18) -> hd1(x18)
   app(tl0(),x20) -> tl1(x20)
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [init0] = 2,
    
    [last0] = 1,
    
    [tl1](x0) = x0 + 1,
    
    [tl0] = 0,
    
    [hd1](x0) = x0 + 2,
    
    [hd0] = 0,
    
    [cons2](x0, x1) = 2x0 + x1,
    
    [cons1](x0) = x0,
    
    [cons0] = 0,
    
    [nil0] = 0,
    
    [reverse22](x0, x1) = x0 + x1,
    
    [reverse21](x0) = x0 + 2,
    
    [reverse20] = 0,
    
    [reverse1](x0) = x0,
    
    [reverse0] = 0,
    
    [compose3](x0, x1, x2) = 4x0 + 4x1 + x2 + 6,
    
    [compose2](x0, x1) = 4x0 + x1 + 1,
    
    [compose1](x0) = x0 + 2,
    
    [compose0] = 2,
    
    [app](x0, x1) = 4x0 + x1 + 3
   orientation:
    compose3(f,g,x) = 4f + 4g + x + 6 >= 4f + 4g + x + 6 = app(g,app(f,x))
    
    reverse1(l) = l >= l = reverse22(l,nil0())
    
    reverse22(nil0(),l) = l >= l = l
    
    reverse22(cons2(x,xs),l) = l + 2x + xs >= l + 2x + xs = reverse22(xs,cons2(x,l))
    
    hd1(cons2(x,xs)) = 2x + xs + 2 >= x = x
    
    tl1(cons2(x,xs)) = 2x + xs + 1 >= xs = xs
    
    last0() = 1 >= 1 = compose2(hd0(),reverse0())
    
    init0() = 2 >= 2 = compose2(reverse0(),compose2(tl0(),reverse0()))
    
    app(compose2(x5,x6),x7) = 16x5 + 4x6 + x7 + 7 >= 4x5 + 4x6 + x7 + 6 = compose3(x5,x6,x7)
    
    app(compose1(x5),x6) = 4x5 + x6 + 11 >= 4x5 + x6 + 1 = compose2(x5,x6)
    
    app(compose0(),x5) = x5 + 11 >= x5 + 2 = compose1(x5)
    
    app(reverse0(),x9) = x9 + 3 >= x9 = reverse1(x9)
    
    app(reverse21(x11),x12) = 4x11 + x12 + 11 >= x11 + x12 = reverse22(x11,x12)
    
    app(reverse20(),x11) = x11 + 3 >= x11 + 2 = reverse21(x11)
    
    app(cons1(x15),x16) = 4x15 + x16 + 3 >= 2x15 + x16 = cons2(x15,x16)
    
    app(cons0(),x15) = x15 + 3 >= x15 = cons1(x15)
    
    app(hd0(),x18) = x18 + 3 >= x18 + 2 = hd1(x18)
    
    app(tl0(),x20) = x20 + 3 >= x20 + 1 = tl1(x20)
   problem:
    compose3(f,g,x) -> app(g,app(f,x))
    reverse1(l) -> reverse22(l,nil0())
    reverse22(nil0(),l) -> l
    reverse22(cons2(x,xs),l) -> reverse22(xs,cons2(x,l))
    last0() -> compose2(hd0(),reverse0())
    init0() -> compose2(reverse0(),compose2(tl0(),reverse0()))
   Matrix Interpretation Processor: dim=3
    
    interpretation:
               [1]
     [init0] = [0]
               [1],
     
               [0]
     [last0] = [0]
               [0],
     
             [0]
     [tl0] = [0]
             [0],
     
             [0]
     [hd0] = [0]
             [0],
     
                       [1 0 1]     [1 0 0]     [0]
     [cons2](x0, x1) = [0 0 0]x0 + [0 1 0]x1 + [1]
                       [0 0 0]     [0 0 0]     [0],
     
              [0]
     [nil0] = [1]
              [0],
     
                           [1 1 0]       
     [reverse22](x0, x1) = [0 1 0]x0 + x1
                           [0 1 0]       ,
     
                      [1 1 0]     [0]
     [reverse1](x0) = [0 1 1]x0 + [1]
                      [0 1 0]     [0],
     
                  [0]
     [reverse0] = [0]
                  [1],
     
                              [1 0 0]     [1 0 0]     [1 0 0]  
     [compose3](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2
                              [0 0 0]     [0 0 0]     [0 0 0]  ,
     
                          [1 0 1]     [1 0 0]  
     [compose2](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                          [0 0 1]     [0 0 0]  ,
     
                     [1 0 0]     [1 0 0]  
     [app](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                     [0 0 0]     [0 0 0]  
    orientation:
                       [1 0 0]    [1 0 0]    [1 0 0]     [1 0 0]    [1 0 0]    [1 0 0]                   
     compose3(f,g,x) = [0 0 0]f + [0 0 0]g + [0 0 0]x >= [0 0 0]f + [0 0 0]g + [0 0 0]x = app(g,app(f,x))
                       [0 0 0]    [0 0 0]    [0 0 0]     [0 0 0]    [0 0 0]    [0 0 0]                   
     
                   [1 1 0]    [0]    [1 1 0]    [0]                      
     reverse1(l) = [0 1 1]l + [1] >= [0 1 0]l + [1] = reverse22(l,nil0())
                   [0 1 0]    [0]    [0 1 0]    [0]                      
     
                               [1]         
     reverse22(nil0(),l) = l + [1] >= l = l
                               [1]         
     
                                    [1 0 1]    [1 1 0]     [1]    [1 0 0]    [1 0 1]    [1 1 0]     [0]                           
     reverse22(cons2(x,xs),l) = l + [0 0 0]x + [0 1 0]xs + [1] >= [0 1 0]l + [0 0 0]x + [0 1 0]xs + [1] = reverse22(xs,cons2(x,l))
                                    [0 0 0]    [0 1 0]     [1]    [0 0 0]    [0 0 0]    [0 1 0]     [0]                           
     
               [0]    [0]                             
     last0() = [0] >= [0] = compose2(hd0(),reverse0())
               [0]    [0]                             
     
               [1]    [1]                                                  
     init0() = [0] >= [0] = compose2(reverse0(),compose2(tl0(),reverse0()))
               [1]    [1]                                                  
    problem:
     compose3(f,g,x) -> app(g,app(f,x))
     reverse1(l) -> reverse22(l,nil0())
     last0() -> compose2(hd0(),reverse0())
     init0() -> compose2(reverse0(),compose2(tl0(),reverse0()))
    Matrix Interpretation Processor: dim=3
     
     interpretation:
                [1]
      [init0] = [0]
                [0],
      
                [0]
      [last0] = [0]
                [0],
      
              [0]
      [tl0] = [0]
              [0],
      
              [0]
      [hd0] = [0]
              [0],
      
               [0]
      [nil0] = [0]
               [0],
      
                            [1 0 0]     [1 0 0]  
      [reverse22](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                            [0 0 0]     [0 0 0]  ,
      
                       [1 0 0]  
      [reverse1](x0) = [0 0 0]x0
                       [0 0 0]  ,
      
                   [0]
      [reverse0] = [0]
                   [0],
      
                               [1 0 0]     [1 0 0]     [1 0 0]     [0]
      [compose3](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [1]
                               [0 0 0]     [0 0 0]     [0 0 0]     [0],
      
                           [1 0 0]     [1 0 0]  
      [compose2](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                           [0 0 0]     [0 0 0]  ,
      
                      [1 0 0]     [1 0 0]     [0]
      [app](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1]
                      [0 0 0]     [0 0 0]     [0]
     orientation:
                        [1 0 0]    [1 0 0]    [1 0 0]    [0]    [1 0 0]    [1 0 0]    [1 0 0]    [0]                  
      compose3(f,g,x) = [0 0 0]f + [0 0 0]g + [0 0 0]x + [1] >= [0 0 0]f + [0 0 0]g + [0 0 0]x + [1] = app(g,app(f,x))
                        [0 0 0]    [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0 0 0]    [0]                  
      
                    [1 0 0]     [1 0 0]                       
      reverse1(l) = [0 0 0]l >= [0 0 0]l = reverse22(l,nil0())
                    [0 0 0]     [0 0 0]                       
      
                [0]    [0]                             
      last0() = [0] >= [0] = compose2(hd0(),reverse0())
                [0]    [0]                             
      
                [1]    [0]                                                  
      init0() = [0] >= [0] = compose2(reverse0(),compose2(tl0(),reverse0()))
                [0]    [0]                                                  
     problem:
      compose3(f,g,x) -> app(g,app(f,x))
      reverse1(l) -> reverse22(l,nil0())
      last0() -> compose2(hd0(),reverse0())
     Matrix Interpretation Processor: dim=3
      
      interpretation:
                 [1]
       [last0] = [1]
                 [0],
       
               [0]
       [hd0] = [0]
               [1],
       
                [0]
       [nil0] = [0]
                [0],
       
                             [1 0 0]     [1 0 0]  
       [reverse22](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                             [0 0 0]     [0 0 0]  ,
       
                        [1 0 0]  
       [reverse1](x0) = [0 0 0]x0
                        [0 0 0]  ,
       
                    [0]
       [reverse0] = [0]
                    [0],
       
                                [1 0 0]     [1 0 0]     [1 0 0]  
       [compose3](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2
                                [0 0 0]     [0 0 0]     [0 0 0]  ,
       
                            [1 0 0]     [1 0 0]  
       [compose2](x0, x1) = [0 0 1]x0 + [0 0 0]x1
                            [0 0 0]     [0 0 0]  ,
       
                       [1 0 0]     [1 0 0]  
       [app](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                       [0 0 0]     [0 0 0]  
      orientation:
                         [1 0 0]    [1 0 0]    [1 0 0]     [1 0 0]    [1 0 0]    [1 0 0]                   
       compose3(f,g,x) = [0 0 0]f + [0 0 0]g + [0 0 0]x >= [0 0 0]f + [0 0 0]g + [0 0 0]x = app(g,app(f,x))
                         [0 0 0]    [0 0 0]    [0 0 0]     [0 0 0]    [0 0 0]    [0 0 0]                   
       
                     [1 0 0]     [1 0 0]                       
       reverse1(l) = [0 0 0]l >= [0 0 0]l = reverse22(l,nil0())
                     [0 0 0]     [0 0 0]                       
       
                 [1]    [0]                             
       last0() = [1] >= [1] = compose2(hd0(),reverse0())
                 [0]    [0]                             
      problem:
       compose3(f,g,x) -> app(g,app(f,x))
       reverse1(l) -> reverse22(l,nil0())
      Matrix Interpretation Processor: dim=3
       
       interpretation:
                 [0]
        [nil0] = [0]
                 [0],
        
                              [1 0 0]     [1 0 0]  
        [reverse22](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                              [0 0 0]     [0 0 0]  ,
        
                         [1 0 0]     [1]
        [reverse1](x0) = [0 0 0]x0 + [0]
                         [0 0 0]     [0],
        
                                 [1 0 0]     [1 0 1]     [1 0 0]  
        [compose3](x0, x1, x2) = [0 0 0]x0 + [1 1 0]x1 + [1 0 0]x2
                                 [1 0 0]     [0 0 0]     [1 0 0]  ,
        
                        [1 0 0]     [1 0 0]  
        [app](x0, x1) = [0 0 0]x0 + [0 0 1]x1
                        [0 0 0]     [1 0 0]  
       orientation:
                          [1 0 0]    [1 0 1]    [1 0 0]     [1 0 0]    [1 0 0]    [1 0 0]                   
        compose3(f,g,x) = [0 0 0]f + [1 1 0]g + [1 0 0]x >= [0 0 0]f + [0 0 0]g + [1 0 0]x = app(g,app(f,x))
                          [1 0 0]    [0 0 0]    [1 0 0]     [1 0 0]    [0 0 0]    [1 0 0]                   
        
                      [1 0 0]    [1]    [1 0 0]                       
        reverse1(l) = [0 0 0]l + [0] >= [0 0 0]l = reverse22(l,nil0())
                      [0 0 0]    [0]    [0 0 0]                       
       problem:
        compose3(f,g,x) -> app(g,app(f,x))
       Matrix Interpretation Processor: dim=3
        
        interpretation:
                                  [1 0 0]     [1 0 0]     [1 0 0]     [1]
         [compose3](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [0]
                                  [0 0 0]     [0 0 0]     [0 0 0]     [0],
         
                         [1 0 0]     [1 0 0]  
         [app](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                         [0 0 0]     [0 0 0]  
        orientation:
                           [1 0 0]    [1 0 0]    [1 0 0]    [1]    [1 0 0]    [1 0 0]    [1 0 0]                   
         compose3(f,g,x) = [0 0 0]f + [0 0 0]g + [0 0 0]x + [0] >= [0 0 0]f + [0 0 0]g + [0 0 0]x = app(g,app(f,x))
                           [0 0 0]    [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0 0 0]                   
        problem:
         
        Qed