YES(?,PRIMREC)

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

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

The input was oriented with the instance of'multiset path order' as
induced by the precedence

 prime > 0, prime > false, prime > prime1, prime > and, prime > not,
 prime > divp, prime > =, prime > rem, s > 0, s > false, s > prime1,
 s > and, s > not, s > divp, s > =, s > rem, prime1 > 0,
 prime1 > false, prime1 > and, prime1 > not, prime1 > divp,
 prime1 > =, prime1 > rem, true > 0, true > false, true > prime1,
 true > and, true > not, true > divp, true > =, true > rem, and > 0,
 and > false, and > =, and > rem, not > 0, not > false, not > =,
 not > rem, divp > 0, divp > false, divp > =, divp > rem, prime ~ s,
 prime ~ true, 0 ~ false, 0 ~ =, 0 ~ rem, false ~ =, false ~ rem,
 s ~ true, and ~ not, and ~ divp, not ~ divp, = ~ rem .

Hurray, we answered YES(?,PRIMREC)