YES(?,O(n^3))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^3)).

Strict 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()
  , prime1(x, s(s(y))) -> and(not(divp(s(s(y)), x)), prime1(x, s(y)))
  , divp(x, y) -> =(rem(x, y), 0()) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^3))

The input was oriented with the instance of 'Small Polynomial Path
Order (PS)' as induced by the safe mapping

 safe(prime) = {}, safe(0) = {}, safe(false) = {}, safe(s) = {1},
 safe(prime1) = {}, safe(true) = {}, safe(and) = {1, 2},
 safe(not) = {1}, safe(divp) = {1, 2}, safe(=) = {1, 2},
 safe(rem) = {1, 2}

and precedence

 prime > prime1, prime > divp, prime1 > divp .

Following symbols are considered recursive:

 {prime, prime1, divp}

The recursion depth is 3.

For your convenience, here are the satisfied ordering constraints:

               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);))
                                                                                        
             divp(; x,  y) > =(; rem(; x,  y),  0())                                    
                                                                                        

Hurray, we answered YES(?,O(n^3))