Problem SK90 2.29

YES(?,ELEMENTARY)

We consider the following Problem:

  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())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,ELEMENTARY)

Proof:
  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) = {2}, safe(=) = {1, 2},
   safe(rem) = {1, 2}
  
  and precedence
  
   prime > prime1, prime1 > divp .
  
  Following symbols are considered recursive:
  
   {prime, prime1}
  
  The recursion depth is 2 .
  
  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):
  
   Strict DPs: {}
   Weak DPs  : {}
   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())}
   Weak Trs  : {}

Hurray, we answered YES(?,ELEMENTARY)

YES(?,PRIMREC)

We consider the following Problem:

  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())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,PRIMREC)

Proof:
  The input was oriented with the instance of
  'multiset path orders' as induced by the precedence
  
   prime > false, prime > prime1, prime1 > false, prime1 > and,
   prime1 > not, prime1 > divp, divp > =, divp > rem, 0 ~ divp,
   s ~ true .

Hurray, we answered YES(?,PRIMREC)

YES(?,POLY)

We consider the following Problem:

  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())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,POLY)

Proof:
  The input was oriented with the instance of
  Polynomial Path Order () as induced by the safe mapping
  
   safe(prime) = {}, safe(0) = {}, safe(false) = {}, safe(s) = {1},
   safe(prime1) = {1}, safe(true) = {}, safe(and) = {1, 2},
   safe(not) = {1}, safe(divp) = {1, 2}, safe(=) = {1, 2},
   safe(rem) = {1, 2}
  
  and precedence
  
   prime > prime1, prime1 > divp .
  
  Following symbols are considered recursive:
  
   {prime, prime1}
  
  The recursion depth is 2 .
  
  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):
  
   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  prime(0();) -> false()
      , prime(s(; 0());) -> false()
      , prime(s(; s(; x));) -> prime1(s(; x); s(; s(; x)))
      , prime1(0(); x) -> false()
      , prime1(s(; 0()); x) -> true()
      , prime1(s(; s(; y)); x) ->
        and(; not(; divp(; s(; s(; y)), x)), prime1(s(; y); x))
      , divp(; x, y) -> =(; rem(; x, y), 0())}
   Weak Trs  : {}

Hurray, we answered YES(?,POLY)

YES(?,POLY)

We consider the following Problem:

  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())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,POLY)

Proof:
  The input was oriented with the instance of
  Polynomial Path Order (PS) as induced by the safe mapping
  
   safe(prime) = {}, safe(0) = {}, safe(false) = {}, safe(s) = {1},
   safe(prime1) = {1}, safe(true) = {}, safe(and) = {1, 2},
   safe(not) = {1}, safe(divp) = {1, 2}, safe(=) = {1, 2},
   safe(rem) = {1, 2}
  
  and precedence
  
   prime > prime1, prime1 > divp .
  
  Following symbols are considered recursive:
  
   {prime, prime1}
  
  The recursion depth is 2 .
  
  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):
  
   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  prime(0();) -> false()
      , prime(s(; 0());) -> false()
      , prime(s(; s(; x));) -> prime1(s(; x); s(; s(; x)))
      , prime1(0(); x) -> false()
      , prime1(s(; 0()); x) -> true()
      , prime1(s(; s(; y)); x) ->
        and(; not(; divp(; s(; s(; y)), x)), prime1(s(; y); x))
      , divp(; x, y) -> =(; rem(; x, y), 0())}
   Weak Trs  : {}

Hurray, we answered YES(?,POLY)

YES(?,O(n^1))

We consider the following Problem:

  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())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^1))

Proof:
  The input was oriented with the instance of
  Small Polynomial Path Order (WSC,
                             Nat 1-bounded) 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, prime1 > divp .
  
  Following symbols are considered recursive:
  
   {prime1}
  
  The recursion depth is 1 .
  
  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):
  
   Strict DPs: {}
   Weak DPs  : {}
   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())}
   Weak Trs  : {}

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

YES(?,O(n^1))

We consider the following Problem:

  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())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^1))

Proof:
  The input was oriented with the instance of
  Small Polynomial Path Order (WSC,
                             PS) as induced by the safe mapping
  
   safe(prime) = {}, safe(0) = {}, safe(false) = {}, safe(s) = {1},
   safe(prime1) = {1}, safe(true) = {}, safe(and) = {1, 2},
   safe(not) = {1}, safe(divp) = {1, 2}, safe(=) = {1, 2},
   safe(rem) = {1, 2}
  
  and precedence
  
   prime1 > divp, prime ~ prime1 .
  
  Following symbols are considered recursive:
  
   {prime, prime1}
  
  The recursion depth is 1 .
  
  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):
  
   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  prime(0();) -> false()
      , prime(s(; 0());) -> false()
      , prime(s(; s(; x));) -> prime1(s(; x); s(; s(; x)))
      , prime1(0(); x) -> false()
      , prime1(s(; 0()); x) -> true()
      , prime1(s(; s(; y)); x) ->
        and(; not(; divp(; s(; s(; y)), x)), prime1(s(; y); x))
      , divp(; x, y) -> =(; rem(; x, y), 0())}
   Weak Trs  : {}

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