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:
 Complexity Transformation Processor:
  strict:
   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()))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [init] = 1,
     
     [last] = 0,
     
     [tl] = 0,
     
     [hd] = 0,
     
     [cons] = 0,
     
     [nil] = 0,
     
     [reverse2] = 0,
     
     [reverse] = 0,
     
     [app](x0, x1) = x0 + x1,
     
     [compose] = 0
    orientation:
     app(app(app(compose(),f),g),x) = f + g + x >= f + g + x = app(g,app(f,x))
     
     app(reverse(),l) = l >= l = app(app(reverse2(),l),nil())
     
     app(app(reverse2(),nil()),l) = l >= l = l
     
     app(app(reverse2(),app(app(cons(),x),xs)),l) = l + x + xs >= l + x + xs = app(app(reverse2(),xs),app(app(cons(),x),l))
     
     app(hd(),app(app(cons(),x),xs)) = x + xs >= x = x
     
     app(tl(),app(app(cons(),x),xs)) = x + xs >= xs = xs
     
     last() = 0 >= 0 = app(app(compose(),hd()),reverse())
     
     init() = 1 >= 0 = app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
    problem:
     strict:
      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())
     weak:
      init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [init] = 0,
       
       [last] = 1,
       
       [tl] = 0,
       
       [hd] = 0,
       
       [cons] = 0,
       
       [nil] = 1,
       
       [reverse2] = 0,
       
       [reverse] = 0,
       
       [app](x0, x1) = x0 + x1,
       
       [compose] = 0
      orientation:
       app(app(app(compose(),f),g),x) = f + g + x >= f + g + x = app(g,app(f,x))
       
       app(reverse(),l) = l >= l + 1 = app(app(reverse2(),l),nil())
       
       app(app(reverse2(),nil()),l) = l + 1 >= l = l
       
       app(app(reverse2(),app(app(cons(),x),xs)),l) = l + x + xs >= l + x + xs = app(app(reverse2(),xs),app(app(cons(),x),l))
       
       app(hd(),app(app(cons(),x),xs)) = x + xs >= x = x
       
       app(tl(),app(app(cons(),x),xs)) = x + xs >= xs = xs
       
       last() = 1 >= 0 = app(app(compose(),hd()),reverse())
       
       init() = 0 >= 0 = app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
      problem:
       strict:
        app(app(app(compose(),f),g),x) -> app(g,app(f,x))
        app(reverse(),l) -> app(app(reverse2(),l),nil())
        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
       weak:
        app(app(reverse2(),nil()),l) -> l
        last() -> app(app(compose(),hd()),reverse())
        init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [init] = 1,
         
         [last] = 0,
         
         [tl] = 0,
         
         [hd] = 0,
         
         [cons] = 1,
         
         [nil] = 0,
         
         [reverse2] = 0,
         
         [reverse] = 0,
         
         [app](x0, x1) = x0 + x1,
         
         [compose] = 0
        orientation:
         app(app(app(compose(),f),g),x) = f + g + x >= f + g + x = app(g,app(f,x))
         
         app(reverse(),l) = l >= l = app(app(reverse2(),l),nil())
         
         app(app(reverse2(),app(app(cons(),x),xs)),l) = l + x + xs + 1 >= l + x + xs + 1 = app(app(reverse2(),xs),app(app(cons(),x),l))
         
         app(hd(),app(app(cons(),x),xs)) = x + xs + 1 >= x = x
         
         app(tl(),app(app(cons(),x),xs)) = x + xs + 1 >= xs = xs
         
         app(app(reverse2(),nil()),l) = l >= l = l
         
         last() = 0 >= 0 = app(app(compose(),hd()),reverse())
         
         init() = 1 >= 0 = app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
        problem:
         strict:
          app(app(app(compose(),f),g),x) -> app(g,app(f,x))
          app(reverse(),l) -> app(app(reverse2(),l),nil())
          app(app(reverse2(),app(app(cons(),x),xs)),l) ->
          app(app(reverse2(),xs),app(app(cons(),x),l))
         weak:
          app(hd(),app(app(cons(),x),xs)) -> x
          app(tl(),app(app(cons(),x),xs)) -> xs
          app(app(reverse2(),nil()),l) -> l
          last() -> app(app(compose(),hd()),reverse())
          init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
        Open