WORST_CASE(?,O(n^2))
* Step 1: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            a__app(X1,X2) -> app(X1,X2)
            a__app(cons(X,XS),YS) -> cons(mark(X),app(XS,YS))
            a__app(nil(),YS) -> mark(YS)
            a__from(X) -> cons(mark(X),from(s(X)))
            a__from(X) -> from(X)
            a__prefix(L) -> cons(nil(),zWadr(L,prefix(L)))
            a__prefix(X) -> prefix(X)
            a__zWadr(X1,X2) -> zWadr(X1,X2)
            a__zWadr(XS,nil()) -> nil()
            a__zWadr(cons(X,XS),cons(Y,YS)) -> cons(a__app(mark(Y),cons(mark(X),nil())),zWadr(XS,YS))
            a__zWadr(nil(),YS) -> nil()
            mark(app(X1,X2)) -> a__app(mark(X1),mark(X2))
            mark(cons(X1,X2)) -> cons(mark(X1),X2)
            mark(from(X)) -> a__from(mark(X))
            mark(nil()) -> nil()
            mark(prefix(X)) -> a__prefix(mark(X))
            mark(s(X)) -> s(mark(X))
            mark(zWadr(X1,X2)) -> a__zWadr(mark(X1),mark(X2))
        - Signature:
            {a__app/2,a__from/1,a__prefix/1,a__zWadr/2,mark/1} / {app/2,cons/2,from/1,nil/0,prefix/1,s/1,zWadr/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__app,a__from,a__prefix,a__zWadr
            ,mark} and constructors {app,cons,from,nil,prefix,s,zWadr}
    + Applied Processor:
        NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(a__app) = {1,2},
          uargs(a__from) = {1},
          uargs(a__prefix) = {1},
          uargs(a__zWadr) = {1,2},
          uargs(cons) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {a__app,a__from,a__prefix,a__zWadr,mark}
        TcT has computed the following interpretation:
             p(a__app) = [1 2] x1 + [1 2] x2 + [4]
                         [0 1]      [0 1]      [1]
            p(a__from) = [1 2] x1 + [1]           
                         [0 1]      [4]           
          p(a__prefix) = [1 4] x1 + [5]           
                         [0 1]      [2]           
           p(a__zWadr) = [1 4] x1 + [1 4] x2 + [1]
                         [0 1]      [0 1]      [1]
                p(app) = [1 2] x1 + [1 2] x2 + [3]
                         [0 1]      [0 1]      [1]
               p(cons) = [1 0] x1 + [0]           
                         [0 1]      [1]           
               p(from) = [1 2] x1 + [0]           
                         [0 1]      [4]           
               p(mark) = [1 2] x1 + [0]           
                         [0 1]      [0]           
                p(nil) = [0]                      
                         [1]                      
             p(prefix) = [1 4] x1 + [4]           
                         [0 1]      [2]           
                  p(s) = [1 4] x1 + [0]           
                         [0 1]      [6]           
              p(zWadr) = [1 4] x1 + [1 4] x2 + [0]
                         [0 1]      [0 1]      [1]
        
        Following rules are strictly oriented:
                          a__app(X1,X2) = [1 2] X1 + [1 2] X2 + [4]                             
                                          [0 1]      [0 1]      [1]                             
                                        > [1 2] X1 + [1 2] X2 + [3]                             
                                          [0 1]      [0 1]      [1]                             
                                        = app(X1,X2)                                            
        
                  a__app(cons(X,XS),YS) = [1 2] X + [1 2] YS + [6]                              
                                          [0 1]     [0 1]      [2]                              
                                        > [1 2] X + [0]                                         
                                          [0 1]     [1]                                         
                                        = cons(mark(X),app(XS,YS))                              
        
                       a__app(nil(),YS) = [1 2] YS + [6]                                        
                                          [0 1]      [2]                                        
                                        > [1 2] YS + [0]                                        
                                          [0 1]      [0]                                        
                                        = mark(YS)                                              
        
                             a__from(X) = [1 2] X + [1]                                         
                                          [0 1]     [4]                                         
                                        > [1 2] X + [0]                                         
                                          [0 1]     [1]                                         
                                        = cons(mark(X),from(s(X)))                              
        
                             a__from(X) = [1 2] X + [1]                                         
                                          [0 1]     [4]                                         
                                        > [1 2] X + [0]                                         
                                          [0 1]     [4]                                         
                                        = from(X)                                               
        
                           a__prefix(L) = [1 4] L + [5]                                         
                                          [0 1]     [2]                                         
                                        > [0]                                                   
                                          [2]                                                   
                                        = cons(nil(),zWadr(L,prefix(L)))                        
        
                           a__prefix(X) = [1 4] X + [5]                                         
                                          [0 1]     [2]                                         
                                        > [1 4] X + [4]                                         
                                          [0 1]     [2]                                         
                                        = prefix(X)                                             
        
                        a__zWadr(X1,X2) = [1 4] X1 + [1 4] X2 + [1]                             
                                          [0 1]      [0 1]      [1]                             
                                        > [1 4] X1 + [1 4] X2 + [0]                             
                                          [0 1]      [0 1]      [1]                             
                                        = zWadr(X1,X2)                                          
        
                     a__zWadr(XS,nil()) = [1 4] XS + [5]                                        
                                          [0 1]      [2]                                        
                                        > [0]                                                   
                                          [1]                                                   
                                        = nil()                                                 
        
        a__zWadr(cons(X,XS),cons(Y,YS)) = [1 4] X + [1 4] Y + [9]                               
                                          [0 1]     [0 1]     [3]                               
                                        > [1 4] X + [1 4] Y + [6]                               
                                          [0 1]     [0 1]     [3]                               
                                        = cons(a__app(mark(Y),cons(mark(X),nil())),zWadr(XS,YS))
        
                     a__zWadr(nil(),YS) = [1 4] YS + [5]                                        
                                          [0 1]      [2]                                        
                                        > [0]                                                   
                                          [1]                                                   
                                        = nil()                                                 
        
                       mark(app(X1,X2)) = [1 4] X1 + [1 4] X2 + [5]                             
                                          [0 1]      [0 1]      [1]                             
                                        > [1 4] X1 + [1 4] X2 + [4]                             
                                          [0 1]      [0 1]      [1]                             
                                        = a__app(mark(X1),mark(X2))                             
        
                      mark(cons(X1,X2)) = [1 2] X1 + [2]                                        
                                          [0 1]      [1]                                        
                                        > [1 2] X1 + [0]                                        
                                          [0 1]      [1]                                        
                                        = cons(mark(X1),X2)                                     
        
                          mark(from(X)) = [1 4] X + [8]                                         
                                          [0 1]     [4]                                         
                                        > [1 4] X + [1]                                         
                                          [0 1]     [4]                                         
                                        = a__from(mark(X))                                      
        
                            mark(nil()) = [2]                                                   
                                          [1]                                                   
                                        > [0]                                                   
                                          [1]                                                   
                                        = nil()                                                 
        
                        mark(prefix(X)) = [1 6] X + [8]                                         
                                          [0 1]     [2]                                         
                                        > [1 6] X + [5]                                         
                                          [0 1]     [2]                                         
                                        = a__prefix(mark(X))                                    
        
                             mark(s(X)) = [1 6] X + [12]                                        
                                          [0 1]     [6]                                         
                                        > [1 6] X + [0]                                         
                                          [0 1]     [6]                                         
                                        = s(mark(X))                                            
        
                     mark(zWadr(X1,X2)) = [1 6] X1 + [1 6] X2 + [2]                             
                                          [0 1]      [0 1]      [1]                             
                                        > [1 6] X1 + [1 6] X2 + [1]                             
                                          [0 1]      [0 1]      [1]                             
                                        = a__zWadr(mark(X1),mark(X2))                           
        
        
        Following rules are (at-least) weakly oriented:
        

WORST_CASE(?,O(n^2))