WORST_CASE(?,O(n^1))
* Step 1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            -(x,0()) -> x
            -(s(x),s(y)) -> -(x,y)
            double(0()) -> 0()
            double(s(x)) -> s(s(double(x)))
            half(0()) -> 0()
            half(double(x)) -> x
            half(s(0())) -> 0()
            half(s(s(x))) -> s(half(x))
            if(0(),y,z) -> y
            if(s(x),y,z) -> z
        - Signature:
            {-/2,double/1,half/1,if/3} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {-,double,half,if} and constructors {0,s}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, 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(s) = {1}
        
        Following symbols are considered usable:
          {-,double,half,if}
        TcT has computed the following interpretation:
               p(-) = [5] x1 + [4] x2 + [0]         
               p(0) = [1]                           
          p(double) = [8] x1 + [5]                  
            p(half) = [2] x1 + [3]                  
              p(if) = [6] x1 + [2] x2 + [2] x3 + [4]
               p(s) = [1] x1 + [3]                  
        
        Following rules are strictly oriented:
               -(x,0()) = [5] x + [4]                 
                        > [1] x + [0]                 
                        = x                           
        
           -(s(x),s(y)) = [5] x + [4] y + [27]        
                        > [5] x + [4] y + [0]         
                        = -(x,y)                      
        
            double(0()) = [13]                        
                        > [1]                         
                        = 0()                         
        
           double(s(x)) = [8] x + [29]                
                        > [8] x + [11]                
                        = s(s(double(x)))             
        
              half(0()) = [5]                         
                        > [1]                         
                        = 0()                         
        
        half(double(x)) = [16] x + [13]               
                        > [1] x + [0]                 
                        = x                           
        
           half(s(0())) = [11]                        
                        > [1]                         
                        = 0()                         
        
          half(s(s(x))) = [2] x + [15]                
                        > [2] x + [6]                 
                        = s(half(x))                  
        
            if(0(),y,z) = [2] y + [2] z + [10]        
                        > [1] y + [0]                 
                        = y                           
        
           if(s(x),y,z) = [6] x + [2] y + [2] z + [22]
                        > [1] z + [0]                 
                        = z                           
        
        
        Following rules are (at-least) weakly oriented:
        

WORST_CASE(?,O(n^1))