*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        minus(x,0()) -> x
        minus(s(x),s(y)) -> minus(x,y)
        quot(0(),s(y)) -> 0()
        quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {minus/2,quot/2} / {0/0,s/1}
      Obligation:
        Innermost
        basic terms: {minus,quot}/{0,s}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      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(quot) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
              p(0) = [8]                  
          p(minus) = [1] x1 + [0]         
           p(quot) = [1] x1 + [1] x2 + [0]
              p(s) = [1] x1 + [8]         
        
        Following rules are strictly oriented:
        minus(s(x),s(y)) = [1] x + [8] 
                         > [1] x + [0] 
                         = minus(x,y)  
        
          quot(0(),s(y)) = [1] y + [16]
                         > [8]         
                         = 0()         
        
        
        Following rules are (at-least) weakly oriented:
           minus(x,0()) =  [1] x + [0]             
                        >= [1] x + [0]             
                        =  x                       
        
        quot(s(x),s(y)) =  [1] x + [1] y + [16]    
                        >= [1] x + [1] y + [16]    
                        =  s(quot(minus(x,y),s(y)))
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        minus(x,0()) -> x
        quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
      Weak DP Rules:
        
      Weak TRS Rules:
        minus(s(x),s(y)) -> minus(x,y)
        quot(0(),s(y)) -> 0()
      Signature:
        {minus/2,quot/2} / {0/0,s/1}
      Obligation:
        Innermost
        basic terms: {minus,quot}/{0,s}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      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(quot) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
              p(0) = [2]         
          p(minus) = [1] x1 + [1]
           p(quot) = [1] x1 + [1]
              p(s) = [1] x1 + [1]
        
        Following rules are strictly oriented:
        minus(x,0()) = [1] x + [1]
                     > [1] x + [0]
                     = x          
        
        
        Following rules are (at-least) weakly oriented:
        minus(s(x),s(y)) =  [1] x + [2]             
                         >= [1] x + [1]             
                         =  minus(x,y)              
        
          quot(0(),s(y)) =  [3]                     
                         >= [2]                     
                         =  0()                     
        
         quot(s(x),s(y)) =  [1] x + [2]             
                         >= [1] x + [3]             
                         =  s(quot(minus(x,y),s(y)))
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
      Weak DP Rules:
        
      Weak TRS Rules:
        minus(x,0()) -> x
        minus(s(x),s(y)) -> minus(x,y)
        quot(0(),s(y)) -> 0()
      Signature:
        {minus/2,quot/2} / {0/0,s/1}
      Obligation:
        Innermost
        basic terms: {minus,quot}/{0,s}
    Applied Processor:
      NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      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) = [2] x1 + [3] x2 + [0]
            p(s) = [1] x1 + [6]         
      
      Following rules are strictly oriented:
      quot(s(x),s(y)) = [2] x + [3] y + [30]    
                      > [2] x + [3] y + [24]    
                      = s(quot(minus(x,y),s(y)))
      
      
      Following rules are (at-least) weakly oriented:
          minus(x,0()) =  [1] x + [0] 
                       >= [1] x + [0] 
                       =  x           
      
      minus(s(x),s(y)) =  [1] x + [6] 
                       >= [1] x + [0] 
                       =  minus(x,y)  
      
        quot(0(),s(y)) =  [3] y + [18]
                       >= [0]         
                       =  0()         
      
*** 1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        minus(x,0()) -> x
        minus(s(x),s(y)) -> minus(x,y)
        quot(0(),s(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
        basic terms: {minus,quot}/{0,s}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).