WORST_CASE(?,O(n^3))
* Step 1: WeightGap WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            ifMinus(false(),s(X),Y) -> s(minus(X,Y))
            ifMinus(true(),s(X),Y) -> 0()
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(0(),Y) -> 0()
            minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y)
            quot(0(),s(Y)) -> 0()
            quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
        - Signature:
            {ifMinus/3,le/2,minus/2,quot/2} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {ifMinus,le,minus,quot} and constructors {0,false,s,true}
    + 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(ifMinus) = {1},
            uargs(quot) = {1},
            uargs(s) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                  p(0) = [0]                  
              p(false) = [9]                  
            p(ifMinus) = [1] x1 + [1] x2 + [6]
                 p(le) = [0]                  
              p(minus) = [1] x1 + [0]         
               p(quot) = [1] x1 + [0]         
                  p(s) = [1] x1 + [10]        
               p(true) = [0]                  
          
          Following rules are strictly oriented:
          ifMinus(false(),s(X),Y) = [1] X + [25] 
                                  > [1] X + [10] 
                                  = s(minus(X,Y))
          
           ifMinus(true(),s(X),Y) = [1] X + [16] 
                                  > [0]          
                                  = 0()          
          
          
          Following rules are (at-least) weakly oriented:
                le(0(),Y) =  [0]                       
                          >= [0]                       
                          =  true()                    
          
             le(s(X),0()) =  [0]                       
                          >= [9]                       
                          =  false()                   
          
            le(s(X),s(Y)) =  [0]                       
                          >= [0]                       
                          =  le(X,Y)                   
          
             minus(0(),Y) =  [0]                       
                          >= [0]                       
                          =  0()                       
          
            minus(s(X),Y) =  [1] X + [10]              
                          >= [1] X + [16]              
                          =  ifMinus(le(s(X),Y),s(X),Y)
          
           quot(0(),s(Y)) =  [0]                       
                          >= [0]                       
                          =  0()                       
          
          quot(s(X),s(Y)) =  [1] X + [10]              
                          >= [1] X + [10]              
                          =  s(quot(minus(X,Y),s(Y)))  
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: NaturalMI WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(0(),Y) -> 0()
            minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y)
            quot(0(),s(Y)) -> 0()
            quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
        - Weak TRS:
            ifMinus(false(),s(X),Y) -> s(minus(X,Y))
            ifMinus(true(),s(X),Y) -> 0()
        - Signature:
            {ifMinus/3,le/2,minus/2,quot/2} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {ifMinus,le,minus,quot} and constructors {0,false,s,true}
    + 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(ifMinus) = {1},
          uargs(quot) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {ifMinus,le,minus,quot}
        TcT has computed the following interpretation:
                p(0) = [13]                 
            p(false) = [1]                  
          p(ifMinus) = [1] x1 + [1] x2 + [2]
               p(le) = [1]                  
            p(minus) = [1] x1 + [3]         
             p(quot) = [2] x1 + [1]         
                p(s) = [1] x1 + [10]        
             p(true) = [1]                  
        
        Following rules are strictly oriented:
           minus(0(),Y) = [16]                    
                        > [13]                    
                        = 0()                     
        
         quot(0(),s(Y)) = [27]                    
                        > [13]                    
                        = 0()                     
        
        quot(s(X),s(Y)) = [2] X + [21]            
                        > [2] X + [17]            
                        = s(quot(minus(X,Y),s(Y)))
        
        
        Following rules are (at-least) weakly oriented:
        ifMinus(false(),s(X),Y) =  [1] X + [13]              
                                >= [1] X + [13]              
                                =  s(minus(X,Y))             
        
         ifMinus(true(),s(X),Y) =  [1] X + [13]              
                                >= [13]                      
                                =  0()                       
        
                      le(0(),Y) =  [1]                       
                                >= [1]                       
                                =  true()                    
        
                   le(s(X),0()) =  [1]                       
                                >= [1]                       
                                =  false()                   
        
                  le(s(X),s(Y)) =  [1]                       
                                >= [1]                       
                                =  le(X,Y)                   
        
                  minus(s(X),Y) =  [1] X + [13]              
                                >= [1] X + [13]              
                                =  ifMinus(le(s(X),Y),s(X),Y)
        
* Step 3: WeightGap WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y)
        - Weak TRS:
            ifMinus(false(),s(X),Y) -> s(minus(X,Y))
            ifMinus(true(),s(X),Y) -> 0()
            minus(0(),Y) -> 0()
            quot(0(),s(Y)) -> 0()
            quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
        - Signature:
            {ifMinus/3,le/2,minus/2,quot/2} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {ifMinus,le,minus,quot} and constructors {0,false,s,true}
    + 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(ifMinus) = {1},
            uargs(quot) = {1},
            uargs(s) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                  p(0) = [0]                  
              p(false) = [7]                  
            p(ifMinus) = [1] x1 + [1]         
                 p(le) = [9]                  
              p(minus) = [0]                  
               p(quot) = [1] x1 + [2] x2 + [7]
                  p(s) = [1] x1 + [8]         
               p(true) = [0]                  
          
          Following rules are strictly oriented:
             le(0(),Y) = [9]    
                       > [0]    
                       = true() 
          
          le(s(X),0()) = [9]    
                       > [7]    
                       = false()
          
          
          Following rules are (at-least) weakly oriented:
          ifMinus(false(),s(X),Y) =  [8]                       
                                  >= [8]                       
                                  =  s(minus(X,Y))             
          
           ifMinus(true(),s(X),Y) =  [1]                       
                                  >= [0]                       
                                  =  0()                       
          
                    le(s(X),s(Y)) =  [9]                       
                                  >= [9]                       
                                  =  le(X,Y)                   
          
                     minus(0(),Y) =  [0]                       
                                  >= [0]                       
                                  =  0()                       
          
                    minus(s(X),Y) =  [0]                       
                                  >= [10]                      
                                  =  ifMinus(le(s(X),Y),s(X),Y)
          
                   quot(0(),s(Y)) =  [2] Y + [23]              
                                  >= [0]                       
                                  =  0()                       
          
                  quot(s(X),s(Y)) =  [1] X + [2] Y + [31]      
                                  >= [2] Y + [31]              
                                  =  s(quot(minus(X,Y),s(Y)))  
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: NaturalMI WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            le(s(X),s(Y)) -> le(X,Y)
            minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y)
        - Weak TRS:
            ifMinus(false(),s(X),Y) -> s(minus(X,Y))
            ifMinus(true(),s(X),Y) -> 0()
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            minus(0(),Y) -> 0()
            quot(0(),s(Y)) -> 0()
            quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
        - Signature:
            {ifMinus/3,le/2,minus/2,quot/2} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {ifMinus,le,minus,quot} and constructors {0,false,s,true}
    + 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(ifMinus) = {1},
          uargs(quot) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {ifMinus,le,minus,quot}
        TcT has computed the following interpretation:
                p(0) = [0]                      
                       [2]                      
            p(false) = [0]                      
                       [0]                      
          p(ifMinus) = [4 0] x1 + [1 2] x2 + [3]
                       [0 0]      [0 1]      [0]
               p(le) = [0]                      
                       [0]                      
            p(minus) = [1 2] x1 + [5]           
                       [0 1]      [0]           
             p(quot) = [2 5] x1 + [0 1] x2 + [0]
                       [0 1]      [0 0]      [0]
                p(s) = [1 4] x1 + [0]           
                       [0 1]      [2]           
             p(true) = [0]                      
                       [0]                      
        
        Following rules are strictly oriented:
        minus(s(X),Y) = [1 6] X + [9]             
                        [0 1]     [2]             
                      > [1 6] X + [7]             
                        [0 1]     [2]             
                      = ifMinus(le(s(X),Y),s(X),Y)
        
        
        Following rules are (at-least) weakly oriented:
        ifMinus(false(),s(X),Y) =  [1 6] X + [7]            
                                   [0 1]     [2]            
                                >= [1 6] X + [5]            
                                   [0 1]     [2]            
                                =  s(minus(X,Y))            
        
         ifMinus(true(),s(X),Y) =  [1 6] X + [7]            
                                   [0 1]     [2]            
                                >= [0]                      
                                   [2]                      
                                =  0()                      
        
                      le(0(),Y) =  [0]                      
                                   [0]                      
                                >= [0]                      
                                   [0]                      
                                =  true()                   
        
                   le(s(X),0()) =  [0]                      
                                   [0]                      
                                >= [0]                      
                                   [0]                      
                                =  false()                  
        
                  le(s(X),s(Y)) =  [0]                      
                                   [0]                      
                                >= [0]                      
                                   [0]                      
                                =  le(X,Y)                  
        
                   minus(0(),Y) =  [9]                      
                                   [2]                      
                                >= [0]                      
                                   [2]                      
                                =  0()                      
        
                 quot(0(),s(Y)) =  [0 1] Y + [12]           
                                   [0 0]     [2]            
                                >= [0]                      
                                   [2]                      
                                =  0()                      
        
                quot(s(X),s(Y)) =  [2 13] X + [0 1] Y + [12]
                                   [0  1]     [0 0]     [2] 
                                >= [2 13] X + [0 1] Y + [12]
                                   [0  1]     [0 0]     [2] 
                                =  s(quot(minus(X,Y),s(Y))) 
        
* Step 5: NaturalMI WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            le(s(X),s(Y)) -> le(X,Y)
        - Weak TRS:
            ifMinus(false(),s(X),Y) -> s(minus(X,Y))
            ifMinus(true(),s(X),Y) -> 0()
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            minus(0(),Y) -> 0()
            minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y)
            quot(0(),s(Y)) -> 0()
            quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
        - Signature:
            {ifMinus/3,le/2,minus/2,quot/2} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {ifMinus,le,minus,quot} and constructors {0,false,s,true}
    + Applied Processor:
        NaturalMI {miDimension = 3, miDegree = 3, 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(ifMinus) = {1},
          uargs(quot) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {ifMinus,le,minus,quot}
        TcT has computed the following interpretation:
                p(0) = [0]                          
                       [0]                          
                       [0]                          
            p(false) = [2]                          
                       [0]                          
                       [0]                          
          p(ifMinus) = [1 0 0]      [1 1 0]      [0]
                       [0 0 0] x1 + [0 1 0] x2 + [0]
                       [0 0 0]      [0 0 1]      [0]
               p(le) = [0 0 1]      [0]             
                       [2 0 0] x1 + [0]             
                       [0 0 0]      [0]             
            p(minus) = [1 1 1]      [0]             
                       [0 1 0] x1 + [0]             
                       [0 0 1]      [0]             
             p(quot) = [2 2 0]      [0 1 0]      [2]
                       [0 1 0] x1 + [0 0 0] x2 + [0]
                       [0 0 1]      [0 0 0]      [0]
                p(s) = [1 2 0]      [0]             
                       [0 1 2] x1 + [0]             
                       [0 0 1]      [2]             
             p(true) = [0]                          
                       [0]                          
                       [0]                          
        
        Following rules are strictly oriented:
        le(s(X),s(Y)) = [0 0 1]     [2]
                        [2 4 0] X + [0]
                        [0 0 0]     [0]
                      > [0 0 1]     [0]
                        [2 0 0] X + [0]
                        [0 0 0]     [0]
                      = le(X,Y)        
        
        
        Following rules are (at-least) weakly oriented:
        ifMinus(false(),s(X),Y) =  [1 3 2]     [2]            
                                   [0 1 2] X + [0]            
                                   [0 0 1]     [2]            
                                >= [1 3 1]     [0]            
                                   [0 1 2] X + [0]            
                                   [0 0 1]     [2]            
                                =  s(minus(X,Y))              
        
         ifMinus(true(),s(X),Y) =  [1 3 2]     [0]            
                                   [0 1 2] X + [0]            
                                   [0 0 1]     [2]            
                                >= [0]                        
                                   [0]                        
                                   [0]                        
                                =  0()                        
        
                      le(0(),Y) =  [0]                        
                                   [0]                        
                                   [0]                        
                                >= [0]                        
                                   [0]                        
                                   [0]                        
                                =  true()                     
        
                   le(s(X),0()) =  [0 0 1]     [2]            
                                   [2 4 0] X + [0]            
                                   [0 0 0]     [0]            
                                >= [2]                        
                                   [0]                        
                                   [0]                        
                                =  false()                    
        
                   minus(0(),Y) =  [0]                        
                                   [0]                        
                                   [0]                        
                                >= [0]                        
                                   [0]                        
                                   [0]                        
                                =  0()                        
        
                  minus(s(X),Y) =  [1 3 3]     [2]            
                                   [0 1 2] X + [0]            
                                   [0 0 1]     [2]            
                                >= [1 3 3]     [2]            
                                   [0 1 2] X + [0]            
                                   [0 0 1]     [2]            
                                =  ifMinus(le(s(X),Y),s(X),Y) 
        
                 quot(0(),s(Y)) =  [0 1 2]     [2]            
                                   [0 0 0] Y + [0]            
                                   [0 0 0]     [0]            
                                >= [0]                        
                                   [0]                        
                                   [0]                        
                                =  0()                        
        
                quot(s(X),s(Y)) =  [2 6 4]     [0 1 2]     [2]
                                   [0 1 2] X + [0 0 0] Y + [0]
                                   [0 0 1]     [0 0 0]     [2]
                                >= [2 6 2]     [0 1 2]     [2]
                                   [0 1 2] X + [0 0 0] Y + [0]
                                   [0 0 1]     [0 0 0]     [2]
                                =  s(quot(minus(X,Y),s(Y)))   
        
* Step 6: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            ifMinus(false(),s(X),Y) -> s(minus(X,Y))
            ifMinus(true(),s(X),Y) -> 0()
            le(0(),Y) -> true()
            le(s(X),0()) -> false()
            le(s(X),s(Y)) -> le(X,Y)
            minus(0(),Y) -> 0()
            minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y)
            quot(0(),s(Y)) -> 0()
            quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
        - Signature:
            {ifMinus/3,le/2,minus/2,quot/2} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {ifMinus,le,minus,quot} and constructors {0,false,s,true}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^3))