WORST_CASE(Omega(n^1),O(n^1))
* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
    + Considered Problem:
        - Strict TRS:
            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:
            innermost runtime complexity wrt. defined symbols {divp,prime,prime1} and constructors {0,=,and,false,not
            ,rem,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            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:
            innermost runtime complexity wrt. defined symbols {divp,prime,prime1} and constructors {0,=,and,false,not
            ,rem,s,true}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          prime1(x,s(y)){y -> s(y)} =
            prime1(x,s(s(y))) ->^+ and(not(divp(s(s(y)),x)),prime1(x,s(y)))
              = C[prime1(x,s(y)) = prime1(x,s(y)){}]

** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            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:
            innermost runtime complexity wrt. defined symbols {divp,prime,prime1} and constructors {0,=,and,false,not
            ,rem,s,true}
    + 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(and) = {1,2},
          uargs(not) = {1}
        
        Following symbols are considered usable:
          {divp,prime,prime1}
        TcT has computed the following interpretation:
               p(0) = 0       
               p(=) = x2      
             p(and) = x1 + x2 
            p(divp) = 0       
           p(false) = 0       
             p(not) = x1      
           p(prime) = 12      
          p(prime1) = 2 + 9*x1
             p(rem) = 0       
               p(s) = 0       
            p(true) = 0       
        
        Following rules are strictly oriented:
              prime(0()) = 12                  
                         > 0                   
                         = false()             
        
           prime(s(0())) = 12                  
                         > 0                   
                         = false()             
        
          prime(s(s(x))) = 12                  
                         > 2                   
                         = prime1(s(s(x)),s(x))
        
           prime1(x,0()) = 2 + 9*x             
                         > 0                   
                         = false()             
        
        prime1(x,s(0())) = 2 + 9*x             
                         > 0                   
                         = true()              
        
        
        Following rules are (at-least) weakly oriented:
                divp(x,y) =  0                                       
                          >= 0                                       
                          =  =(rem(x,y),0())                         
        
        prime1(x,s(s(y))) =  2 + 9*x                                 
                          >= 2 + 9*x                                 
                          =  and(not(divp(s(s(y)),x)),prime1(x,s(y)))
        
** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            divp(x,y) -> =(rem(x,y),0())
            prime1(x,s(s(y))) -> and(not(divp(s(s(y)),x)),prime1(x,s(y)))
        - Weak TRS:
            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()
        - Signature:
            {divp/2,prime/1,prime1/2} / {0/0,=/2,and/2,false/0,not/1,rem/2,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {divp,prime,prime1} and constructors {0,=,and,false,not
            ,rem,s,true}
    + 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(and) = {1,2},
          uargs(not) = {1}
        
        Following symbols are considered usable:
          {divp,prime,prime1}
        TcT has computed the following interpretation:
               p(0) = 0          
               p(=) = 1          
             p(and) = 2 + x1 + x2
            p(divp) = 4          
           p(false) = 0          
             p(not) = x1         
           p(prime) = 2 + 10*x1  
          p(prime1) = 2 + 8*x2   
             p(rem) = 1 + x2     
               p(s) = 1 + x1     
            p(true) = 4          
        
        Following rules are strictly oriented:
                divp(x,y) = 4                                       
                          > 1                                       
                          = =(rem(x,y),0())                         
        
        prime1(x,s(s(y))) = 18 + 8*y                                
                          > 16 + 8*y                                
                          = and(not(divp(s(s(y)),x)),prime1(x,s(y)))
        
        
        Following rules are (at-least) weakly oriented:
              prime(0()) =  2                   
                         >= 0                   
                         =  false()             
        
           prime(s(0())) =  12                  
                         >= 0                   
                         =  false()             
        
          prime(s(s(x))) =  22 + 10*x           
                         >= 10 + 8*x            
                         =  prime1(s(s(x)),s(x))
        
           prime1(x,0()) =  2                   
                         >= 0                   
                         =  false()             
        
        prime1(x,s(0())) =  10                  
                         >= 4                   
                         =  true()              
        
** Step 1.b:3: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            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:
            innermost runtime complexity wrt. defined symbols {divp,prime,prime1} and constructors {0,=,and,false,not
            ,rem,s,true}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(Omega(n^1),O(n^1))