YES(?,ELEMENTARY)

We are left with following problem, upon which TcT provides the
certificate YES(?,ELEMENTARY).

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(?,ELEMENTARY)

The input was oriented with the instance of 'Lightweight Multiset
Path Order' 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) = {}, 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(?,ELEMENTARY)