WORST_CASE(?,O(n^1))
* Step 1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            minus(x,0()) -> x
            minus(s(x),s(y)) -> minus(x,y)
            quot(0(),y) -> 0()
            quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
        - Signature:
            {minus/2,quot/2} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {minus,quot} and constructors {0,s}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, 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(quot) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {minus,quot}
        TcT has computed the following interpretation:
              p(0) = [0]                  
          p(minus) = [1] x1 + [0]         
           p(quot) = [1] x1 + [8] x2 + [2]
              p(s) = [1] x1 + [0]         
        
        Following rules are strictly oriented:
        quot(0(),y) = [8] y + [2]
                    > [0]        
                    = 0()        
        
        
        Following rules are (at-least) weakly oriented:
            minus(x,0()) =  [1] x + [0]             
                         >= [1] x + [0]             
                         =  x                       
        
        minus(s(x),s(y)) =  [1] x + [0]             
                         >= [1] x + [0]             
                         =  minus(x,y)              
        
         quot(s(x),s(y)) =  [1] x + [8] y + [2]     
                         >= [1] x + [8] y + [2]     
                         =  s(quot(minus(x,y),s(y)))
        
* Step 2: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            minus(x,0()) -> x
            minus(s(x),s(y)) -> minus(x,y)
            quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
        - Weak TRS:
            quot(0(),y) -> 0()
        - Signature:
            {minus/2,quot/2} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {minus,quot} and constructors {0,s}
    + Applied Processor:
        NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(linear):
        The following argument positions are considered usable:
          uargs(quot) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {minus,quot}
        TcT has computed the following interpretation:
              p(0) = 0     
          p(minus) = x1    
           p(quot) = 4 + x1
              p(s) = 8 + x1
        
        Following rules are strictly oriented:
        minus(s(x),s(y)) = 8 + x     
                         > x         
                         = minus(x,y)
        
        
        Following rules are (at-least) weakly oriented:
           minus(x,0()) =  x                       
                        >= x                       
                        =  x                       
        
            quot(0(),y) =  4                       
                        >= 0                       
                        =  0()                     
        
        quot(s(x),s(y)) =  12 + x                  
                        >= 12 + x                  
                        =  s(quot(minus(x,y),s(y)))
        
* Step 3: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            minus(x,0()) -> x
            quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
        - Weak TRS:
            minus(s(x),s(y)) -> minus(x,y)
            quot(0(),y) -> 0()
        - Signature:
            {minus/2,quot/2} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {minus,quot} and constructors {0,s}
    + Applied Processor:
        NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(linear):
        The following argument positions are considered usable:
          uargs(quot) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {minus,quot}
        TcT has computed the following interpretation:
              p(0) = 5     
          p(minus) = x1    
           p(quot) = 4*x1  
              p(s) = 2 + x1
        
        Following rules are strictly oriented:
        quot(s(x),s(y)) = 8 + 4*x                 
                        > 2 + 4*x                 
                        = s(quot(minus(x,y),s(y)))
        
        
        Following rules are (at-least) weakly oriented:
            minus(x,0()) =  x         
                         >= x         
                         =  x         
        
        minus(s(x),s(y)) =  2 + x     
                         >= x         
                         =  minus(x,y)
        
             quot(0(),y) =  20        
                         >= 5         
                         =  0()       
        
* Step 4: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            minus(x,0()) -> x
        - Weak TRS:
            minus(s(x),s(y)) -> minus(x,y)
            quot(0(),y) -> 0()
            quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
        - Signature:
            {minus/2,quot/2} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {minus,quot} and constructors {0,s}
    + Applied Processor:
        NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(linear):
        The following argument positions are considered usable:
          uargs(quot) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {minus,quot}
        TcT has computed the following interpretation:
              p(0) = 0     
          p(minus) = 1 + x1
           p(quot) = 8*x1  
              p(s) = 2 + x1
        
        Following rules are strictly oriented:
        minus(x,0()) = 1 + x
                     > x    
                     = x    
        
        
        Following rules are (at-least) weakly oriented:
        minus(s(x),s(y)) =  3 + x                   
                         >= 1 + x                   
                         =  minus(x,y)              
        
             quot(0(),y) =  0                       
                         >= 0                       
                         =  0()                     
        
         quot(s(x),s(y)) =  16 + 8*x                
                         >= 10 + 8*x                
                         =  s(quot(minus(x,y),s(y)))
        
* Step 5: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            minus(x,0()) -> x
            minus(s(x),s(y)) -> minus(x,y)
            quot(0(),y) -> 0()
            quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
        - Signature:
            {minus/2,quot/2} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {minus,quot} and constructors {0,s}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))