WORST_CASE(?,O(n^2))
* Step 1: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            -(x,0()) -> x
            -(0(),s(y)) -> 0()
            -(s(x),s(y)) -> -(x,y)
            div(x,0()) -> 0()
            div(0(),y) -> 0()
            div(s(x),s(y)) -> if(lt(x,y),0(),s(div(-(x,y),s(y))))
            if(false(),x,y) -> y
            if(true(),x,y) -> x
            lt(x,0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),s(y)) -> lt(x,y)
        - Signature:
            {-/2,div/2,if/3,lt/2} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {-,div,if,lt} and constructors {0,false,s,true}
    + 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(div) = {1},
          uargs(if) = {1,3},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {-,div,if,lt}
        TcT has computed the following interpretation:
              p(-) = [1 1] x1 + [1]                      
                     [0 1]      [0]                      
              p(0) = [0]                                 
                     [0]                                 
            p(div) = [2 5] x1 + [2 0] x2 + [4]           
                     [0 1]      [0 0]      [0]           
          p(false) = [0]                                 
                     [0]                                 
             p(if) = [1 0] x1 + [1 1] x2 + [1 0] x3 + [1]
                     [0 0]      [1 4]      [0 1]      [0]
             p(lt) = [0 2] x1 + [0 0] x2 + [1]           
                     [0 0]      [0 2]      [0]           
              p(s) = [1 4] x1 + [0]                      
                     [0 1]      [1]                      
           p(true) = [0]                                 
                     [0]                                 
        
        Following rules are strictly oriented:
               -(x,0()) = [1 1] x + [1]                      
                          [0 1]     [0]                      
                        > [1 0] x + [0]                      
                          [0 1]     [0]                      
                        = x                                  
        
            -(0(),s(y)) = [1]                                
                          [0]                                
                        > [0]                                
                          [0]                                
                        = 0()                                
        
           -(s(x),s(y)) = [1 5] x + [2]                      
                          [0 1]     [1]                      
                        > [1 1] x + [1]                      
                          [0 1]     [0]                      
                        = -(x,y)                             
        
             div(x,0()) = [2 5] x + [4]                      
                          [0 1]     [0]                      
                        > [0]                                
                          [0]                                
                        = 0()                                
        
             div(0(),y) = [2 0] y + [4]                      
                          [0 0]     [0]                      
                        > [0]                                
                          [0]                                
                        = 0()                                
        
         div(s(x),s(y)) = [2 13] x + [2 8] y + [9]           
                          [0  1]     [0 0]     [1]           
                        > [2 13] x + [2 8] y + [8]           
                          [0  1]     [0 0]     [1]           
                        = if(lt(x,y),0(),s(div(-(x,y),s(y))))
        
        if(false(),x,y) = [1 1] x + [1 0] y + [1]            
                          [1 4]     [0 1]     [0]            
                        > [1 0] y + [0]                      
                          [0 1]     [0]                      
                        = y                                  
        
         if(true(),x,y) = [1 1] x + [1 0] y + [1]            
                          [1 4]     [0 1]     [0]            
                        > [1 0] x + [0]                      
                          [0 1]     [0]                      
                        = x                                  
        
              lt(x,0()) = [0 2] x + [1]                      
                          [0 0]     [0]                      
                        > [0]                                
                          [0]                                
                        = false()                            
        
           lt(0(),s(y)) = [0 0] y + [1]                      
                          [0 2]     [2]                      
                        > [0]                                
                          [0]                                
                        = true()                             
        
          lt(s(x),s(y)) = [0 2] x + [0 0] y + [3]            
                          [0 0]     [0 2]     [2]            
                        > [0 2] x + [0 0] y + [1]            
                          [0 0]     [0 2]     [0]            
                        = lt(x,y)                            
        
        
        Following rules are (at-least) weakly oriented:
        

WORST_CASE(?,O(n^2))