MAYBE

Problem:
 app(nil(),y) -> y
 app(add(n,x),y) -> add(n,app(x,y))
 reverse(nil()) -> nil()
 reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
 shuffle(nil()) -> nil()
 shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))

Proof:
 RT Transformation Processor:
  strict:
   app(nil(),y) -> y
   app(add(n,x),y) -> add(n,app(x,y))
   reverse(nil()) -> nil()
   reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
   shuffle(nil()) -> nil()
   shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [shuffle](x0) = x0 + 20,
    
    [reverse](x0) = x0 + 18,
    
    [add](x0, x1) = x0 + x1 + 17,
    
    [app](x0, x1) = x0 + x1,
    
    [nil] = 4
   orientation:
    app(nil(),y) = y + 4 >= y = y
    
    app(add(n,x),y) = n + x + y + 17 >= n + x + y + 17 = add(n,app(x,y))
    
    reverse(nil()) = 22 >= 4 = nil()
    
    reverse(add(n,x)) = n + x + 35 >= n + x + 39 = app(reverse(x),add(n,nil()))
    
    shuffle(nil()) = 24 >= 4 = nil()
    
    shuffle(add(n,x)) = n + x + 37 >= n + x + 55 = add(n,shuffle(reverse(x)))
   problem:
    strict:
     app(add(n,x),y) -> add(n,app(x,y))
     reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
     shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
    weak:
     app(nil(),y) -> y
     reverse(nil()) -> nil()
     shuffle(nil()) -> nil()
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
                     [1 4]  
     [shuffle](x0) = [0 1]x0,
     
                       
     [reverse](x0) = x0,
     
                     [1 1]          [0]
     [add](x0, x1) = [0 0]x0 + x1 + [1],
     
                            
     [app](x0, x1) = x0 + x1,
     
             [0]
     [nil] = [0]
    orientation:
                       [1 1]            [0]    [1 1]            [0]                  
     app(add(n,x),y) = [0 0]n + x + y + [1] >= [0 0]n + x + y + [1] = add(n,app(x,y))
     
                         [1 1]        [0]    [1 1]        [0]                               
     reverse(add(n,x)) = [0 0]n + x + [1] >= [0 0]n + x + [1] = app(reverse(x),add(n,nil()))
     
                         [1 1]    [1 4]    [4]    [1 1]    [1 4]    [0]                             
     shuffle(add(n,x)) = [0 0]n + [0 1]x + [1] >= [0 0]n + [0 1]x + [1] = add(n,shuffle(reverse(x)))
     
                              
     app(nil(),y) = y >= y = y
     
                      [0]    [0]        
     reverse(nil()) = [0] >= [0] = nil()
     
                      [0]    [0]        
     shuffle(nil()) = [0] >= [0] = nil()
    problem:
     strict:
      app(add(n,x),y) -> add(n,app(x,y))
      reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
     weak:
      shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
      app(nil(),y) -> y
      reverse(nil()) -> nil()
      shuffle(nil()) -> nil()
    Open