MAYBE

Problem:
 app(nil(),xs) -> nil()
 app(cons(x,xs),ys) -> cons(x,app(xs,ys))
 rev(nil()) -> nil()
 rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))

Proof:
 Complexity Transformation Processor:
  strict:
   app(nil(),xs) -> nil()
   app(cons(x,xs),ys) -> cons(x,app(xs,ys))
   rev(nil()) -> nil()
   rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [append](x0, x1) = x0 + x1,
     
     [rev](x0) = x0,
     
     [cons](x0, x1) = x0 + x1,
     
     [app](x0, x1) = x0 + x1 + 1,
     
     [nil] = 1
    orientation:
     app(nil(),xs) = xs + 2 >= 1 = nil()
     
     app(cons(x,xs),ys) = x + xs + ys + 1 >= x + xs + ys + 1 = cons(x,app(xs,ys))
     
     rev(nil()) = 1 >= 1 = nil()
     
     rev(cons(x,xs)) = x + xs >= x + xs + 1 = append(xs,rev(cons(x,nil())))
    problem:
     strict:
      app(cons(x,xs),ys) -> cons(x,app(xs,ys))
      rev(nil()) -> nil()
      rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
     weak:
      app(nil(),xs) -> nil()
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [append](x0, x1) = x0 + x1,
       
       [rev](x0) = x0 + 1,
       
       [cons](x0, x1) = x0 + x1,
       
       [app](x0, x1) = x0 + x1,
       
       [nil] = 0
      orientation:
       app(cons(x,xs),ys) = x + xs + ys >= x + xs + ys = cons(x,app(xs,ys))
       
       rev(nil()) = 1 >= 0 = nil()
       
       rev(cons(x,xs)) = x + xs + 1 >= x + xs + 1 = append(xs,rev(cons(x,nil())))
       
       app(nil(),xs) = xs >= 0 = nil()
      problem:
       strict:
        app(cons(x,xs),ys) -> cons(x,app(xs,ys))
        rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
       weak:
        rev(nil()) -> nil()
        app(nil(),xs) -> nil()
      Bounds Processor:
       bound: 1
       enrichment: match
       automaton:
        final states: {5,4}
        transitions:
         cons1(2,36) -> 37*
         cons1(1,6) -> 6,4
         cons1(1,10) -> 6,4
         cons1(1,36) -> 41*
         cons1(3,6) -> 6,4
         cons1(3,10) -> 6,4
         cons1(3,36) -> 37*
         cons1(2,6) -> 6,4
         cons1(2,10) -> 6,4
         app1(3,1) -> 6*
         app1(3,3) -> 6*
         app1(1,2) -> 6*
         app1(2,1) -> 6*
         app1(2,3) -> 10*
         app1(3,2) -> 6*
         app1(1,1) -> 6*
         app1(1,3) -> 6*
         app1(2,2) -> 6*
         append1(2,38) -> 5*
         append1(2,42) -> 5*
         append1(36,38) -> 38*
         append1(36,42) -> 42*
         append1(1,38) -> 5*
         append1(1,42) -> 5*
         append1(3,38) -> 5*
         append1(3,42) -> 5*
         rev1(37) -> 38*
         rev1(41) -> 42*
         nil1() -> 6,36
         app0(3,1) -> 4*
         app0(3,3) -> 4*
         app0(1,2) -> 4*
         app0(2,1) -> 4*
         app0(2,3) -> 4*
         app0(3,2) -> 4*
         app0(1,1) -> 4*
         app0(1,3) -> 4*
         app0(2,2) -> 4*
         cons0(3,1) -> 1*
         cons0(3,3) -> 1*
         cons0(1,2) -> 1*
         cons0(2,1) -> 1*
         cons0(2,3) -> 1*
         cons0(3,2) -> 1*
         cons0(1,1) -> 1*
         cons0(1,3) -> 1*
         cons0(2,2) -> 1*
         rev0(2) -> 5*
         rev0(1) -> 5*
         rev0(3) -> 5*
         append0(3,1) -> 2*
         append0(3,3) -> 2*
         append0(1,2) -> 2*
         append0(2,1) -> 2*
         append0(2,3) -> 2*
         append0(3,2) -> 2*
         append0(1,1) -> 2*
         append0(1,3) -> 2*
         append0(2,2) -> 2*
         nil0() -> 4,5,3
       problem:
        strict:
         rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
        weak:
         app(cons(x,xs),ys) -> cons(x,app(xs,ys))
         rev(nil()) -> nil()
         app(nil(),xs) -> nil()
       Open