*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        divp(x,y) -> =(rem(x,y),0())
        prime(0()) -> false()
        prime(s(0())) -> false()
        prime(s(s(x))) -> prime1(s(s(x)),s(x))
        prime1(x,0()) -> false()
        prime1(x,s(0())) -> true()
        prime1(x,s(s(y))) -> and(not(divp(s(s(y)),x)),prime1(x,s(y)))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {divp/2,prime/1,prime1/2} / {0/0,=/2,and/2,false/0,not/1,rem/2,s/1,true/0}
      Obligation:
        Full
        basic terms: {divp,prime,prime1}/{0,=,and,false,not,rem,s,true}
    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(and) = {1,2},
          uargs(not) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
               p(0) = [0]                  
               p(=) = [0]                  
             p(and) = [1] x1 + [1] x2 + [2]
            p(divp) = [0]                  
           p(false) = [0]                  
             p(not) = [1] x1 + [1]         
           p(prime) = [1] x1 + [4]         
          p(prime1) = [1] x2 + [13]        
             p(rem) = [1] x2 + [0]         
               p(s) = [1] x1 + [4]         
            p(true) = [0]                  
        
        Following rules are strictly oriented:
               prime(0()) = [4]                     
                          > [0]                     
                          = false()                 
        
            prime(s(0())) = [8]                     
                          > [0]                     
                          = false()                 
        
            prime1(x,0()) = [13]                    
                          > [0]                     
                          = false()                 
        
         prime1(x,s(0())) = [17]                    
                          > [0]                     
                          = true()                  
        
        prime1(x,s(s(y))) = [1] y + [21]            
                          > [1] y + [20]            
                          = and(not(divp(s(s(y)),x))
                               ,prime1(x,s(y)))     
        
        
        Following rules are (at-least) weakly oriented:
             divp(x,y) =  [0]                 
                       >= [0]                 
                       =  =(rem(x,y),0())     
        
        prime(s(s(x))) =  [1] x + [12]        
                       >= [1] x + [17]        
                       =  prime1(s(s(x)),s(x))
        
      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:
        divp(x,y) -> =(rem(x,y),0())
        prime(s(s(x))) -> prime1(s(s(x)),s(x))
      Weak DP Rules:
        
      Weak TRS Rules:
        prime(0()) -> false()
        prime(s(0())) -> false()
        prime1(x,0()) -> false()
        prime1(x,s(0())) -> true()
        prime1(x,s(s(y))) -> and(not(divp(s(s(y)),x)),prime1(x,s(y)))
      Signature:
        {divp/2,prime/1,prime1/2} / {0/0,=/2,and/2,false/0,not/1,rem/2,s/1,true/0}
      Obligation:
        Full
        basic terms: {divp,prime,prime1}/{0,=,and,false,not,rem,s,true}
    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(and) = {1,2},
        uargs(not) = {1}
      
      Following symbols are considered usable:
        {}
      TcT has computed the following interpretation:
             p(0) = [2]                  
             p(=) = [0]                  
           p(and) = [1] x1 + [1] x2 + [0]
          p(divp) = [8]                  
         p(false) = [2]                  
           p(not) = [1] x1 + [0]         
         p(prime) = [8] x1 + [0]         
        p(prime1) = [8] x2 + [4]         
           p(rem) = [1] x2 + [1]         
             p(s) = [1] x1 + [1]         
          p(true) = [2]                  
      
      Following rules are strictly oriented:
           divp(x,y) = [8]                 
                     > [0]                 
                     = =(rem(x,y),0())     
      
      prime(s(s(x))) = [8] x + [16]        
                     > [8] x + [12]        
                     = prime1(s(s(x)),s(x))
      
      
      Following rules are (at-least) weakly oriented:
             prime(0()) =  [16]                    
                        >= [2]                     
                        =  false()                 
      
          prime(s(0())) =  [24]                    
                        >= [2]                     
                        =  false()                 
      
          prime1(x,0()) =  [20]                    
                        >= [2]                     
                        =  false()                 
      
       prime1(x,s(0())) =  [28]                    
                        >= [2]                     
                        =  true()                  
      
      prime1(x,s(s(y))) =  [8] y + [20]            
                        >= [8] y + [20]            
                        =  and(not(divp(s(s(y)),x))
                              ,prime1(x,s(y)))     
      
*** 1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        divp(x,y) -> =(rem(x,y),0())
        prime(0()) -> false()
        prime(s(0())) -> false()
        prime(s(s(x))) -> prime1(s(s(x)),s(x))
        prime1(x,0()) -> false()
        prime1(x,s(0())) -> true()
        prime1(x,s(s(y))) -> and(not(divp(s(s(y)),x)),prime1(x,s(y)))
      Signature:
        {divp/2,prime/1,prime1/2} / {0/0,=/2,and/2,false/0,not/1,rem/2,s/1,true/0}
      Obligation:
        Full
        basic terms: {divp,prime,prime1}/{0,=,and,false,not,rem,s,true}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).