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())))
 shuffle(nil()) -> nil()
 shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))

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())))
   shuffle(nil()) -> nil()
   shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [shuffle](x0) = x0,
     
     [append](x0, x1) = x0 + x1,
     
     [rev](x0) = x0,
     
     [cons](x0, x1) = x0 + x1,
     
     [app](x0, x1) = x0 + x1 + 1,
     
     [nil] = 0
    orientation:
     app(nil(),xs) = xs + 1 >= 0 = nil()
     
     app(cons(x,xs),ys) = x + xs + ys + 1 >= x + xs + ys + 1 = cons(x,app(xs,ys))
     
     rev(nil()) = 0 >= 0 = nil()
     
     rev(cons(x,xs)) = x + xs >= x + xs = append(xs,rev(cons(x,nil())))
     
     shuffle(nil()) = 0 >= 0 = nil()
     
     shuffle(cons(x,xs)) = x + xs >= x + xs = cons(x,shuffle(rev(xs)))
    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())))
      shuffle(nil()) -> nil()
      shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
     weak:
      app(nil(),xs) -> nil()
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [shuffle](x0) = x0 + 1,
       
       [append](x0, x1) = x0 + x1,
       
       [rev](x0) = x0,
       
       [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()) = 0 >= 0 = nil()
       
       rev(cons(x,xs)) = x + xs >= x + xs = append(xs,rev(cons(x,nil())))
       
       shuffle(nil()) = 1 >= 0 = nil()
       
       shuffle(cons(x,xs)) = x + xs + 1 >= x + xs + 1 = cons(x,shuffle(rev(xs)))
       
       app(nil(),xs) = xs >= 0 = 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())))
        shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
       weak:
        shuffle(nil()) -> nil()
        app(nil(),xs) -> nil()
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [shuffle](x0) = x0 + 1,
         
         [append](x0, x1) = x0 + x1 + 1,
         
         [rev](x0) = x0 + 1,
         
         [cons](x0, x1) = x0 + x1,
         
         [app](x0, x1) = x0 + x1,
         
         [nil] = 1
        orientation:
         app(cons(x,xs),ys) = x + xs + ys >= x + xs + ys = cons(x,app(xs,ys))
         
         rev(nil()) = 2 >= 1 = nil()
         
         rev(cons(x,xs)) = x + xs + 1 >= x + xs + 3 = append(xs,rev(cons(x,nil())))
         
         shuffle(cons(x,xs)) = x + xs + 1 >= x + xs + 2 = cons(x,shuffle(rev(xs)))
         
         shuffle(nil()) = 2 >= 1 = nil()
         
         app(nil(),xs) = xs + 1 >= 1 = nil()
        problem:
         strict:
          app(cons(x,xs),ys) -> cons(x,app(xs,ys))
          rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
          shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
         weak:
          rev(nil()) -> nil()
          shuffle(nil()) -> nil()
          app(nil(),xs) -> nil()
        Bounds Processor:
         bound: 1
         enrichment: match
         automaton:
          final states: {6,5,4}
          transitions:
           cons1(2,12) -> 6*
           cons1(2,26) -> 27*
           cons1(3,17) -> 6*
           cons1(1,12) -> 6*
           cons1(1,26) -> 31*
           cons1(2,17) -> 6*
           cons1(3,12) -> 6*
           cons1(3,26) -> 27*
           cons1(1,17) -> 6*
           append1(2,28) -> 11,5
           append1(2,32) -> 11,5
           append1(26,28) -> 28*
           append1(26,32) -> 32*
           append1(1,28) -> 11,5
           append1(1,32) -> 11,5
           append1(3,28) -> 11,5
           append1(3,32) -> 11,5
           rev1(27) -> 28*
           rev1(2) -> 16*
           rev1(31) -> 32*
           rev1(1) -> 11*
           rev1(3) -> 11*
           nil1() -> 12,11,26
           shuffle1(16) -> 17*
           shuffle1(11) -> 12*
           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(1,4) -> 4*
           cons0(2,1) -> 1*
           cons0(2,3) -> 1*
           cons0(3,2) -> 1*
           cons0(3,4) -> 4*
           cons0(1,1) -> 1*
           cons0(1,3) -> 1*
           cons0(2,2) -> 1*
           cons0(2,4) -> 4*
           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,6,5,3
           shuffle0(2) -> 6*
           shuffle0(1) -> 6*
           shuffle0(3) -> 6*
         problem:
          strict:
           app(cons(x,xs),ys) -> cons(x,app(xs,ys))
           rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
          weak:
           shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
           rev(nil()) -> nil()
           shuffle(nil()) -> nil()
           app(nil(),xs) -> nil()
         Bounds Processor:
          bound: 1
          enrichment: match
          automaton:
           final states: {6,5,4}
           transitions:
            cons1(1,37) -> 42*
            cons1(3,7) -> 7,4
            cons1(3,11) -> 7,4
            cons1(1,53) -> 6*
            cons1(1,57) -> 6*
            cons1(3,37) -> 38*
            cons1(3,53) -> 6*
            cons1(3,57) -> 6*
            cons1(2,7) -> 7,4
            cons1(2,11) -> 7,4
            cons1(2,37) -> 38*
            cons1(2,53) -> 6*
            cons1(2,57) -> 6*
            cons1(1,7) -> 7,4
            cons1(1,11) -> 7,4
            app1(3,1) -> 7*
            app1(3,3) -> 7*
            app1(1,2) -> 7*
            app1(2,1) -> 7*
            app1(2,3) -> 11*
            app1(3,2) -> 7*
            app1(1,1) -> 7*
            app1(1,3) -> 7*
            app1(2,2) -> 7*
            append1(1,39) -> 52,5
            append1(1,43) -> 52,5
            append1(3,39) -> 52,5
            append1(3,43) -> 52,5
            append1(37,39) -> 39*
            append1(37,43) -> 43*
            append1(2,39) -> 52,5
            append1(2,43) -> 52,5
            rev1(42) -> 43*
            rev1(2) -> 56*
            rev1(1) -> 52*
            rev1(38) -> 39*
            rev1(3) -> 52*
            nil1() -> 53,52,7,37
            shuffle1(52) -> 53*
            shuffle1(56) -> 57*
            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,6,5,3
            shuffle0(2) -> 6*
            shuffle0(1) -> 6*
            shuffle0(3) -> 6*
          problem:
           strict:
            rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
           weak:
            app(cons(x,xs),ys) -> cons(x,app(xs,ys))
            shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
            rev(nil()) -> nil()
            shuffle(nil()) -> nil()
            app(nil(),xs) -> nil()
          Open