WORST_CASE(?,O(n^2))
* Step 1: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add(0(),y) -> y
            add(s(x),y) -> s(add(x,y))
            mtadd(x,cons(t,ts)) -> cons(tadd(x,t),mtadd(x,ts))
            mtadd(x,nil()) -> nil()
            tadd(x,leaf()) -> leaf()
            tadd(x,node(y,ts)) -> node(add(x,y),mtadd(x,ts))
        - Signature:
            {add/2,mtadd/2,tadd/2} / {0/0,cons/2,leaf/0,nil/0,node/2,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add,mtadd,tadd} and constructors {0,cons,leaf,nil,node,s}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(cons) = {1,2},
          uargs(node) = {1,2},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {add,mtadd,tadd}
        TcT has computed the following interpretation:
              p(0) = 0                               
            p(add) = 6 + 2*x1 + 2*x2                 
           p(cons) = 3 + x1 + x2                     
           p(leaf) = 0                               
          p(mtadd) = 3 + 3*x1*x2 + x2^2              
            p(nil) = 0                               
           p(node) = 2 + x1 + x2                     
              p(s) = 1 + x1                          
           p(tadd) = 1 + 3*x1 + 3*x1*x2 + 5*x2 + x2^2
        
        Following rules are strictly oriented:
                 add(0(),y) = 6 + 2*y                                                     
                            > y                                                           
                            = y                                                           
        
                add(s(x),y) = 8 + 2*x + 2*y                                               
                            > 7 + 2*x + 2*y                                               
                            = s(add(x,y))                                                 
        
        mtadd(x,cons(t,ts)) = 12 + 6*t + 2*t*ts + 3*t*x + t^2 + 6*ts + 3*ts*x + ts^2 + 9*x
                            > 7 + 5*t + 3*t*x + t^2 + 3*ts*x + ts^2 + 3*x                 
                            = cons(tadd(x,t),mtadd(x,ts))                                 
        
             mtadd(x,nil()) = 3                                                           
                            > 0                                                           
                            = nil()                                                       
        
             tadd(x,leaf()) = 1 + 3*x                                                     
                            > 0                                                           
                            = leaf()                                                      
        
         tadd(x,node(y,ts)) = 15 + 9*ts + 3*ts*x + 2*ts*y + ts^2 + 9*x + 3*x*y + 9*y + y^2
                            > 11 + 3*ts*x + ts^2 + 2*x + 2*y                              
                            = node(add(x,y),mtadd(x,ts))                                  
        
        
        Following rules are (at-least) weakly oriented:
        
* Step 2: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            add(0(),y) -> y
            add(s(x),y) -> s(add(x,y))
            mtadd(x,cons(t,ts)) -> cons(tadd(x,t),mtadd(x,ts))
            mtadd(x,nil()) -> nil()
            tadd(x,leaf()) -> leaf()
            tadd(x,node(y,ts)) -> node(add(x,y),mtadd(x,ts))
        - Signature:
            {add/2,mtadd/2,tadd/2} / {0/0,cons/2,leaf/0,nil/0,node/2,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add,mtadd,tadd} and constructors {0,cons,leaf,nil,node,s}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))