WORST_CASE(?,O(n^2))
* Step 1: WeightGap 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:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          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:
            all
          TcT has computed the following interpretation:
               p(a__app) = [1] x1 + [1] x2 + [4]
              p(a__from) = [1] x1 + [0]         
            p(a__prefix) = [1] x1 + [0]         
             p(a__zWadr) = [1] x1 + [1] x2 + [0]
                  p(app) = [0]                  
                 p(cons) = [1] x1 + [0]         
                 p(from) = [1] x1 + [0]         
                 p(mark) = [0]                  
                  p(nil) = [0]                  
               p(prefix) = [1] x1 + [0]         
                    p(s) = [1] x1 + [0]         
                p(zWadr) = [1] x1 + [1] x2 + [0]
          
          Following rules are strictly oriented:
                  a__app(X1,X2) = [1] X1 + [1] X2 + [4]   
                                > [0]                     
                                = app(X1,X2)              
          
          a__app(cons(X,XS),YS) = [1] X + [1] YS + [4]    
                                > [0]                     
                                = cons(mark(X),app(XS,YS))
          
               a__app(nil(),YS) = [1] YS + [4]            
                                > [0]                     
                                = mark(YS)                
          
          
          Following rules are (at-least) weakly oriented:
                               a__from(X) =  [1] X + [0]                                           
                                          >= [0]                                                   
                                          =  cons(mark(X),from(s(X)))                              
          
                               a__from(X) =  [1] X + [0]                                           
                                          >= [1] X + [0]                                           
                                          =  from(X)                                               
          
                             a__prefix(L) =  [1] L + [0]                                           
                                          >= [0]                                                   
                                          =  cons(nil(),zWadr(L,prefix(L)))                        
          
                             a__prefix(X) =  [1] X + [0]                                           
                                          >= [1] X + [0]                                           
                                          =  prefix(X)                                             
          
                          a__zWadr(X1,X2) =  [1] X1 + [1] X2 + [0]                                 
                                          >= [1] X1 + [1] X2 + [0]                                 
                                          =  zWadr(X1,X2)                                          
          
                       a__zWadr(XS,nil()) =  [1] XS + [0]                                          
                                          >= [0]                                                   
                                          =  nil()                                                 
          
          a__zWadr(cons(X,XS),cons(Y,YS)) =  [1] X + [1] Y + [0]                                   
                                          >= [4]                                                   
                                          =  cons(a__app(mark(Y),cons(mark(X),nil())),zWadr(XS,YS))
          
                       a__zWadr(nil(),YS) =  [1] YS + [0]                                          
                                          >= [0]                                                   
                                          =  nil()                                                 
          
                         mark(app(X1,X2)) =  [0]                                                   
                                          >= [4]                                                   
                                          =  a__app(mark(X1),mark(X2))                             
          
                        mark(cons(X1,X2)) =  [0]                                                   
                                          >= [0]                                                   
                                          =  cons(mark(X1),X2)                                     
          
                            mark(from(X)) =  [0]                                                   
                                          >= [0]                                                   
                                          =  a__from(mark(X))                                      
          
                              mark(nil()) =  [0]                                                   
                                          >= [0]                                                   
                                          =  nil()                                                 
          
                          mark(prefix(X)) =  [0]                                                   
                                          >= [0]                                                   
                                          =  a__prefix(mark(X))                                    
          
                               mark(s(X)) =  [0]                                                   
                                          >= [0]                                                   
                                          =  s(mark(X))                                            
          
                       mark(zWadr(X1,X2)) =  [0]                                                   
                                          >= [0]                                                   
                                          =  a__zWadr(mark(X1),mark(X2))                           
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            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))
        - Weak 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)
        - 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:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          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:
            all
          TcT has computed the following interpretation:
               p(a__app) = [1] x1 + [1] x2 + [4]
              p(a__from) = [1] x1 + [6]         
            p(a__prefix) = [1] x1 + [0]         
             p(a__zWadr) = [1] x1 + [1] x2 + [7]
                  p(app) = [0]                  
                 p(cons) = [1] x1 + [4]         
                 p(from) = [1] x1 + [0]         
                 p(mark) = [1]                  
                  p(nil) = [0]                  
               p(prefix) = [1] x1 + [0]         
                    p(s) = [1] x1 + [0]         
                p(zWadr) = [1] x1 + [1] x2 + [0]
          
          Following rules are strictly oriented:
                               a__from(X) = [1] X + [6]                                           
                                          > [5]                                                   
                                          = cons(mark(X),from(s(X)))                              
          
                               a__from(X) = [1] X + [6]                                           
                                          > [1] X + [0]                                           
                                          = from(X)                                               
          
                          a__zWadr(X1,X2) = [1] X1 + [1] X2 + [7]                                 
                                          > [1] X1 + [1] X2 + [0]                                 
                                          = zWadr(X1,X2)                                          
          
                       a__zWadr(XS,nil()) = [1] XS + [7]                                          
                                          > [0]                                                   
                                          = nil()                                                 
          
          a__zWadr(cons(X,XS),cons(Y,YS)) = [1] X + [1] Y + [15]                                  
                                          > [14]                                                  
                                          = cons(a__app(mark(Y),cons(mark(X),nil())),zWadr(XS,YS))
          
                       a__zWadr(nil(),YS) = [1] YS + [7]                                          
                                          > [0]                                                   
                                          = nil()                                                 
          
                              mark(nil()) = [1]                                                   
                                          > [0]                                                   
                                          = nil()                                                 
          
          
          Following rules are (at-least) weakly oriented:
                  a__app(X1,X2) =  [1] X1 + [1] X2 + [4]         
                                >= [0]                           
                                =  app(X1,X2)                    
          
          a__app(cons(X,XS),YS) =  [1] X + [1] YS + [8]          
                                >= [5]                           
                                =  cons(mark(X),app(XS,YS))      
          
               a__app(nil(),YS) =  [1] YS + [4]                  
                                >= [1]                           
                                =  mark(YS)                      
          
                   a__prefix(L) =  [1] L + [0]                   
                                >= [4]                           
                                =  cons(nil(),zWadr(L,prefix(L)))
          
                   a__prefix(X) =  [1] X + [0]                   
                                >= [1] X + [0]                   
                                =  prefix(X)                     
          
               mark(app(X1,X2)) =  [1]                           
                                >= [6]                           
                                =  a__app(mark(X1),mark(X2))     
          
              mark(cons(X1,X2)) =  [1]                           
                                >= [5]                           
                                =  cons(mark(X1),X2)             
          
                  mark(from(X)) =  [1]                           
                                >= [7]                           
                                =  a__from(mark(X))              
          
                mark(prefix(X)) =  [1]                           
                                >= [1]                           
                                =  a__prefix(mark(X))            
          
                     mark(s(X)) =  [1]                           
                                >= [1]                           
                                =  s(mark(X))                    
          
             mark(zWadr(X1,X2)) =  [1]                           
                                >= [9]                           
                                =  a__zWadr(mark(X1),mark(X2))   
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            a__prefix(L) -> cons(nil(),zWadr(L,prefix(L)))
            a__prefix(X) -> prefix(X)
            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(prefix(X)) -> a__prefix(mark(X))
            mark(s(X)) -> s(mark(X))
            mark(zWadr(X1,X2)) -> a__zWadr(mark(X1),mark(X2))
        - Weak 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__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(nil()) -> nil()
        - 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:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          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:
            all
          TcT has computed the following interpretation:
               p(a__app) = [1] x1 + [1] x2 + [0]
              p(a__from) = [1] x1 + [0]         
            p(a__prefix) = [1] x1 + [4]         
             p(a__zWadr) = [1] x1 + [1] x2 + [0]
                  p(app) = [1] x1 + [1] x2 + [0]
                 p(cons) = [1] x1 + [0]         
                 p(from) = [1] x1 + [0]         
                 p(mark) = [0]                  
                  p(nil) = [0]                  
               p(prefix) = [0]                  
                    p(s) = [1] x1 + [3]         
                p(zWadr) = [1] x1 + [1] x2 + [0]
          
          Following rules are strictly oriented:
          a__prefix(L) = [1] L + [4]                   
                       > [0]                           
                       = cons(nil(),zWadr(L,prefix(L)))
          
          a__prefix(X) = [1] X + [4]                   
                       > [0]                           
                       = prefix(X)                     
          
          
          Following rules are (at-least) weakly oriented:
                            a__app(X1,X2) =  [1] X1 + [1] X2 + [0]                                 
                                          >= [1] X1 + [1] X2 + [0]                                 
                                          =  app(X1,X2)                                            
          
                    a__app(cons(X,XS),YS) =  [1] X + [1] YS + [0]                                  
                                          >= [0]                                                   
                                          =  cons(mark(X),app(XS,YS))                              
          
                         a__app(nil(),YS) =  [1] YS + [0]                                          
                                          >= [0]                                                   
                                          =  mark(YS)                                              
          
                               a__from(X) =  [1] X + [0]                                           
                                          >= [0]                                                   
                                          =  cons(mark(X),from(s(X)))                              
          
                               a__from(X) =  [1] X + [0]                                           
                                          >= [1] X + [0]                                           
                                          =  from(X)                                               
          
                          a__zWadr(X1,X2) =  [1] X1 + [1] X2 + [0]                                 
                                          >= [1] X1 + [1] X2 + [0]                                 
                                          =  zWadr(X1,X2)                                          
          
                       a__zWadr(XS,nil()) =  [1] XS + [0]                                          
                                          >= [0]                                                   
                                          =  nil()                                                 
          
          a__zWadr(cons(X,XS),cons(Y,YS)) =  [1] X + [1] Y + [0]                                   
                                          >= [0]                                                   
                                          =  cons(a__app(mark(Y),cons(mark(X),nil())),zWadr(XS,YS))
          
                       a__zWadr(nil(),YS) =  [1] YS + [0]                                          
                                          >= [0]                                                   
                                          =  nil()                                                 
          
                         mark(app(X1,X2)) =  [0]                                                   
                                          >= [0]                                                   
                                          =  a__app(mark(X1),mark(X2))                             
          
                        mark(cons(X1,X2)) =  [0]                                                   
                                          >= [0]                                                   
                                          =  cons(mark(X1),X2)                                     
          
                            mark(from(X)) =  [0]                                                   
                                          >= [0]                                                   
                                          =  a__from(mark(X))                                      
          
                              mark(nil()) =  [0]                                                   
                                          >= [0]                                                   
                                          =  nil()                                                 
          
                          mark(prefix(X)) =  [0]                                                   
                                          >= [4]                                                   
                                          =  a__prefix(mark(X))                                    
          
                               mark(s(X)) =  [0]                                                   
                                          >= [3]                                                   
                                          =  s(mark(X))                                            
          
                       mark(zWadr(X1,X2)) =  [0]                                                   
                                          >= [0]                                                   
                                          =  a__zWadr(mark(X1),mark(X2))                           
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            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(prefix(X)) -> a__prefix(mark(X))
            mark(s(X)) -> s(mark(X))
            mark(zWadr(X1,X2)) -> a__zWadr(mark(X1),mark(X2))
        - Weak 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(nil()) -> nil()
        - 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 = Just any strict-rules}
    + 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 1] x1 + [1 1] x2 + [3]
                         [0 1]      [0 1]      [0]
            p(a__from) = [1 1] x1 + [4]           
                         [0 1]      [1]           
          p(a__prefix) = [1 4] x1 + [5]           
                         [0 1]      [0]           
           p(a__zWadr) = [1 2] x1 + [1 4] x2 + [3]
                         [0 1]      [0 1]      [0]
                p(app) = [1 1] x1 + [1 1] x2 + [3]
                         [0 1]      [0 1]      [0]
               p(cons) = [1 0] x1 + [4]           
                         [0 1]      [0]           
               p(from) = [1 1] x1 + [4]           
                         [0 1]      [1]           
               p(mark) = [1 1] x1 + [0]           
                         [0 1]      [0]           
                p(nil) = [0]                      
                         [0]                      
             p(prefix) = [1 4] x1 + [5]           
                         [0 1]      [0]           
                  p(s) = [1 2] x1 + [0]           
                         [0 1]      [0]           
              p(zWadr) = [1 2] x1 + [1 4] x2 + [3]
                         [0 1]      [0 1]      [0]
        
        Following rules are strictly oriented:
        mark(from(X)) = [1 2] X + [5]   
                        [0 1]     [1]   
                      > [1 2] X + [4]   
                        [0 1]     [1]   
                      = a__from(mark(X))
        
        
        Following rules are (at-least) weakly oriented:
                          a__app(X1,X2) =  [1 1] X1 + [1 1] X2 + [3]                             
                                           [0 1]      [0 1]      [0]                             
                                        >= [1 1] X1 + [1 1] X2 + [3]                             
                                           [0 1]      [0 1]      [0]                             
                                        =  app(X1,X2)                                            
        
                  a__app(cons(X,XS),YS) =  [1 1] X + [1 1] YS + [7]                              
                                           [0 1]     [0 1]      [0]                              
                                        >= [1 1] X + [4]                                         
                                           [0 1]     [0]                                         
                                        =  cons(mark(X),app(XS,YS))                              
        
                       a__app(nil(),YS) =  [1 1] YS + [3]                                        
                                           [0 1]      [0]                                        
                                        >= [1 1] YS + [0]                                        
                                           [0 1]      [0]                                        
                                        =  mark(YS)                                              
        
                             a__from(X) =  [1 1] X + [4]                                         
                                           [0 1]     [1]                                         
                                        >= [1 1] X + [4]                                         
                                           [0 1]     [0]                                         
                                        =  cons(mark(X),from(s(X)))                              
        
                             a__from(X) =  [1 1] X + [4]                                         
                                           [0 1]     [1]                                         
                                        >= [1 1] X + [4]                                         
                                           [0 1]     [1]                                         
                                        =  from(X)                                               
        
                           a__prefix(L) =  [1 4] L + [5]                                         
                                           [0 1]     [0]                                         
                                        >= [4]                                                   
                                           [0]                                                   
                                        =  cons(nil(),zWadr(L,prefix(L)))                        
        
                           a__prefix(X) =  [1 4] X + [5]                                         
                                           [0 1]     [0]                                         
                                        >= [1 4] X + [5]                                         
                                           [0 1]     [0]                                         
                                        =  prefix(X)                                             
        
                        a__zWadr(X1,X2) =  [1 2] X1 + [1 4] X2 + [3]                             
                                           [0 1]      [0 1]      [0]                             
                                        >= [1 2] X1 + [1 4] X2 + [3]                             
                                           [0 1]      [0 1]      [0]                             
                                        =  zWadr(X1,X2)                                          
        
                     a__zWadr(XS,nil()) =  [1 2] XS + [3]                                        
                                           [0 1]      [0]                                        
                                        >= [0]                                                   
                                           [0]                                                   
                                        =  nil()                                                 
        
        a__zWadr(cons(X,XS),cons(Y,YS)) =  [1 2] X + [1 4] Y + [11]                              
                                           [0 1]     [0 1]     [0]                               
                                        >= [1 2] X + [1 2] Y + [11]                              
                                           [0 1]     [0 1]     [0]                               
                                        =  cons(a__app(mark(Y),cons(mark(X),nil())),zWadr(XS,YS))
        
                     a__zWadr(nil(),YS) =  [1 4] YS + [3]                                        
                                           [0 1]      [0]                                        
                                        >= [0]                                                   
                                           [0]                                                   
                                        =  nil()                                                 
        
                       mark(app(X1,X2)) =  [1 2] X1 + [1 2] X2 + [3]                             
                                           [0 1]      [0 1]      [0]                             
                                        >= [1 2] X1 + [1 2] X2 + [3]                             
                                           [0 1]      [0 1]      [0]                             
                                        =  a__app(mark(X1),mark(X2))                             
        
                      mark(cons(X1,X2)) =  [1 1] X1 + [4]                                        
                                           [0 1]      [0]                                        
                                        >= [1 1] X1 + [4]                                        
                                           [0 1]      [0]                                        
                                        =  cons(mark(X1),X2)                                     
        
                            mark(nil()) =  [0]                                                   
                                           [0]                                                   
                                        >= [0]                                                   
                                           [0]                                                   
                                        =  nil()                                                 
        
                        mark(prefix(X)) =  [1 5] X + [5]                                         
                                           [0 1]     [0]                                         
                                        >= [1 5] X + [5]                                         
                                           [0 1]     [0]                                         
                                        =  a__prefix(mark(X))                                    
        
                             mark(s(X)) =  [1 3] X + [0]                                         
                                           [0 1]     [0]                                         
                                        >= [1 3] X + [0]                                         
                                           [0 1]     [0]                                         
                                        =  s(mark(X))                                            
        
                     mark(zWadr(X1,X2)) =  [1 3] X1 + [1 5] X2 + [3]                             
                                           [0 1]      [0 1]      [0]                             
                                        >= [1 3] X1 + [1 5] X2 + [3]                             
                                           [0 1]      [0 1]      [0]                             
                                        =  a__zWadr(mark(X1),mark(X2))                           
        
* Step 5: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            mark(app(X1,X2)) -> a__app(mark(X1),mark(X2))
            mark(cons(X1,X2)) -> cons(mark(X1),X2)
            mark(prefix(X)) -> a__prefix(mark(X))
            mark(s(X)) -> s(mark(X))
            mark(zWadr(X1,X2)) -> a__zWadr(mark(X1),mark(X2))
        - Weak 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(from(X)) -> a__from(mark(X))
            mark(nil()) -> nil()
        - 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 = Just any strict-rules}
    + 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 + [7]
                         [0 1]      [0 1]      [1]
            p(a__from) = [1 3] x1 + [3]           
                         [0 1]      [1]           
          p(a__prefix) = [1 2] x1 + [5]           
                         [0 1]      [1]           
           p(a__zWadr) = [1 4] x1 + [1 6] x2 + [3]
                         [0 1]      [0 1]      [2]
                p(app) = [1 2] x1 + [1 2] x2 + [7]
                         [0 1]      [0 1]      [1]
               p(cons) = [1 0] x1 + [0 1] x2 + [0]
                         [0 1]      [0 0]      [1]
               p(from) = [1 3] x1 + [1]           
                         [0 1]      [1]           
               p(mark) = [1 2] x1 + [1]           
                         [0 1]      [0]           
                p(nil) = [1]                      
                         [0]                      
             p(prefix) = [1 2] x1 + [4]           
                         [0 1]      [1]           
                  p(s) = [1 2] x1 + [0]           
                         [0 1]      [1]           
              p(zWadr) = [1 4] x1 + [1 6] x2 + [3]
                         [0 1]      [0 1]      [2]
        
        Following rules are strictly oriented:
          mark(app(X1,X2)) = [1 4] X1 + [1 4] X2 + [10] 
                             [0 1]      [0 1]      [1]  
                           > [1 4] X1 + [1 4] X2 + [9]  
                             [0 1]      [0 1]      [1]  
                           = a__app(mark(X1),mark(X2))  
        
         mark(cons(X1,X2)) = [1 2] X1 + [0 1] X2 + [3]  
                             [0 1]      [0 0]      [1]  
                           > [1 2] X1 + [0 1] X2 + [1]  
                             [0 1]      [0 0]      [1]  
                           = cons(mark(X1),X2)          
        
           mark(prefix(X)) = [1 4] X + [7]              
                             [0 1]     [1]              
                           > [1 4] X + [6]              
                             [0 1]     [1]              
                           = a__prefix(mark(X))         
        
                mark(s(X)) = [1 4] X + [3]              
                             [0 1]     [1]              
                           > [1 4] X + [1]              
                             [0 1]     [1]              
                           = s(mark(X))                 
        
        mark(zWadr(X1,X2)) = [1 6] X1 + [1 8] X2 + [8]  
                             [0 1]      [0 1]      [2]  
                           > [1 6] X1 + [1 8] X2 + [5]  
                             [0 1]      [0 1]      [2]  
                           = a__zWadr(mark(X1),mark(X2))
        
        
        Following rules are (at-least) weakly oriented:
                          a__app(X1,X2) =  [1 2] X1 + [1 2] X2 + [7]                             
                                           [0 1]      [0 1]      [1]                             
                                        >= [1 2] X1 + [1 2] X2 + [7]                             
                                           [0 1]      [0 1]      [1]                             
                                        =  app(X1,X2)                                            
        
                  a__app(cons(X,XS),YS) =  [1 2] X + [0 1] XS + [1 2] YS + [9]                   
                                           [0 1]     [0 0]      [0 1]      [2]                   
                                        >= [1 2] X + [0 1] XS + [0 1] YS + [2]                   
                                           [0 1]     [0 0]      [0 0]      [1]                   
                                        =  cons(mark(X),app(XS,YS))                              
        
                       a__app(nil(),YS) =  [1 2] YS + [8]                                        
                                           [0 1]      [1]                                        
                                        >= [1 2] YS + [1]                                        
                                           [0 1]      [0]                                        
                                        =  mark(YS)                                              
        
                             a__from(X) =  [1 3] X + [3]                                         
                                           [0 1]     [1]                                         
                                        >= [1 3] X + [3]                                         
                                           [0 1]     [1]                                         
                                        =  cons(mark(X),from(s(X)))                              
        
                             a__from(X) =  [1 3] X + [3]                                         
                                           [0 1]     [1]                                         
                                        >= [1 3] X + [1]                                         
                                           [0 1]     [1]                                         
                                        =  from(X)                                               
        
                           a__prefix(L) =  [1 2] L + [5]                                         
                                           [0 1]     [1]                                         
                                        >= [0 2] L + [4]                                         
                                           [0 0]     [1]                                         
                                        =  cons(nil(),zWadr(L,prefix(L)))                        
        
                           a__prefix(X) =  [1 2] X + [5]                                         
                                           [0 1]     [1]                                         
                                        >= [1 2] X + [4]                                         
                                           [0 1]     [1]                                         
                                        =  prefix(X)                                             
        
                        a__zWadr(X1,X2) =  [1 4] X1 + [1 6] X2 + [3]                             
                                           [0 1]      [0 1]      [2]                             
                                        >= [1 4] X1 + [1 6] X2 + [3]                             
                                           [0 1]      [0 1]      [2]                             
                                        =  zWadr(X1,X2)                                          
        
                     a__zWadr(XS,nil()) =  [1 4] XS + [4]                                        
                                           [0 1]      [2]                                        
                                        >= [1]                                                   
                                           [0]                                                   
                                        =  nil()                                                 
        
        a__zWadr(cons(X,XS),cons(Y,YS)) =  [1 4] X + [0 1] XS + [1 6] Y + [0 1] YS + [13]        
                                           [0 1]     [0 0]      [0 1]     [0 0]      [4]         
                                        >= [1 4] X + [0 1] XS + [1 4] Y + [0 1] YS + [13]        
                                           [0 1]     [0 0]      [0 1]     [0 0]      [3]         
                                        =  cons(a__app(mark(Y),cons(mark(X),nil())),zWadr(XS,YS))
        
                     a__zWadr(nil(),YS) =  [1 6] YS + [4]                                        
                                           [0 1]      [2]                                        
                                        >= [1]                                                   
                                           [0]                                                   
                                        =  nil()                                                 
        
                          mark(from(X)) =  [1 5] X + [4]                                         
                                           [0 1]     [1]                                         
                                        >= [1 5] X + [4]                                         
                                           [0 1]     [1]                                         
                                        =  a__from(mark(X))                                      
        
                            mark(nil()) =  [2]                                                   
                                           [0]                                                   
                                        >= [1]                                                   
                                           [0]                                                   
                                        =  nil()                                                 
        
* Step 6: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak 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:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))