LMPO

Execution Time (secs)	0.050
Answer	YES(?,ELEMENTARY)
Input	Transformed CSR 04 Ex9 BLR02 L

YES(?,ELEMENTARY)

We consider the following Problem:

  Strict Trs:
    {  filter(cons(X), 0(), M) -> cons(0())
     , filter(cons(X), s(N), M) -> cons(X)
     , sieve(cons(0())) -> cons(0())
     , sieve(cons(s(N))) -> cons(s(N))
     , nats(N) -> cons(N)
     , zprimes() -> sieve(nats(s(s(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(filter) = {1}, safe(cons) = {1}, safe(0) = {}, safe(s) = {1},
   safe(sieve) = {}, safe(nats) = {}, safe(zprimes) = {}

  and precedence

   zprimes > sieve, zprimes > nats .

  Following symbols are considered recursive:

   {}

  The recursion depth is 0 .

  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):

   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  filter(0(), M; cons(; X)) -> cons(; 0())
      , filter(s(; N), M; cons(; X)) -> cons(; X)
      , sieve(cons(; 0());) -> cons(; 0())
      , sieve(cons(; s(; N));) -> cons(; s(; N))
      , nats(N;) -> cons(; N)
      , zprimes() -> sieve(nats(s(; s(; 0())););)}
   Weak Trs  : {}

Hurray, we answered YES(?,ELEMENTARY)

MPO

Execution Time (secs)	0.049
Answer	YES(?,PRIMREC)
Input	Transformed CSR 04 Ex9 BLR02 L

YES(?,PRIMREC)

We consider the following Problem:

  Strict Trs:
    {  filter(cons(X), 0(), M) -> cons(0())
     , filter(cons(X), s(N), M) -> cons(X)
     , sieve(cons(0())) -> cons(0())
     , sieve(cons(s(N))) -> cons(s(N))
     , nats(N) -> cons(N)
     , zprimes() -> sieve(nats(s(s(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

   filter > cons, nats > cons, zprimes > 0, zprimes > s,
   zprimes > sieve, zprimes > nats .

Hurray, we answered YES(?,PRIMREC)

POP*

Execution Time (secs)	0.034
Answer	YES(?,POLY)
Input	Transformed CSR 04 Ex9 BLR02 L

YES(?,POLY)

We consider the following Problem:

  Strict Trs:
    {  filter(cons(X), 0(), M) -> cons(0())
     , filter(cons(X), s(N), M) -> cons(X)
     , sieve(cons(0())) -> cons(0())
     , sieve(cons(s(N))) -> cons(s(N))
     , nats(N) -> cons(N)
     , zprimes() -> sieve(nats(s(s(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(filter) = {1}, safe(cons) = {1}, safe(0) = {}, safe(s) = {1},
   safe(sieve) = {}, safe(nats) = {}, safe(zprimes) = {}

  and precedence

   zprimes > sieve, zprimes > nats .

  Following symbols are considered recursive:

   {}

  The recursion depth is 0 .

  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):

   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  filter(0(), M; cons(; X)) -> cons(; 0())
      , filter(s(; N), M; cons(; X)) -> cons(; X)
      , sieve(cons(; 0());) -> cons(; 0())
      , sieve(cons(; s(; N));) -> cons(; s(; N))
      , nats(N;) -> cons(; N)
      , zprimes() -> sieve(nats(s(; s(; 0())););)}
   Weak Trs  : {}

Hurray, we answered YES(?,POLY)

POP* (PS)

Execution Time (secs)	0.048
Answer	YES(?,POLY)
Input	Transformed CSR 04 Ex9 BLR02 L

YES(?,POLY)

We consider the following Problem:

  Strict Trs:
    {  filter(cons(X), 0(), M) -> cons(0())
     , filter(cons(X), s(N), M) -> cons(X)
     , sieve(cons(0())) -> cons(0())
     , sieve(cons(s(N))) -> cons(s(N))
     , nats(N) -> cons(N)
     , zprimes() -> sieve(nats(s(s(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(filter) = {1}, safe(cons) = {1}, safe(0) = {}, safe(s) = {1},
   safe(sieve) = {}, safe(nats) = {}, safe(zprimes) = {}

  and precedence

   zprimes > sieve, zprimes > nats .

  Following symbols are considered recursive:

   {}

  The recursion depth is 0 .

  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):

   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  filter(0(), M; cons(; X)) -> cons(; 0())
      , filter(s(; N), M; cons(; X)) -> cons(; X)
      , sieve(cons(; 0());) -> cons(; 0())
      , sieve(cons(; s(; N));) -> cons(; s(; N))
      , nats(N;) -> cons(; N)
      , zprimes() -> sieve(nats(s(; s(; 0())););)}
   Weak Trs  : {}

Hurray, we answered YES(?,POLY)

Small POP*

Execution Time (secs)	0.082
Answer	YES(?,O(1))
Input	Transformed CSR 04 Ex9 BLR02 L

YES(?,O(1))

We consider the following Problem:

  Strict Trs:
    {  filter(cons(X), 0(), M) -> cons(0())
     , filter(cons(X), s(N), M) -> cons(X)
     , sieve(cons(0())) -> cons(0())
     , sieve(cons(s(N))) -> cons(s(N))
     , nats(N) -> cons(N)
     , zprimes() -> sieve(nats(s(s(0()))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(1))

Proof:
  The input was oriented with the instance of
  Small Polynomial Path Order (WSC) as induced by the safe mapping

   safe(filter) = {2}, safe(cons) = {1}, safe(0) = {}, safe(s) = {1},
   safe(sieve) = {1}, safe(nats) = {1}, safe(zprimes) = {}

  and precedence

   zprimes > sieve, zprimes > nats .

  Following symbols are considered recursive:

   {}

  The recursion depth is 0 .

  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):

   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  filter(cons(; X), M; 0()) -> cons(; 0())
      , filter(cons(; X), M; s(; N)) -> cons(; X)
      , sieve(; cons(; 0())) -> cons(; 0())
      , sieve(; cons(; s(; N))) -> cons(; s(; N))
      , nats(; N) -> cons(; N)
      , zprimes() -> sieve(; nats(; s(; s(; 0()))))}
   Weak Trs  : {}

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

Small POP* (PS)

Execution Time (secs)	0.043
Answer	YES(?,O(1))
Input	Transformed CSR 04 Ex9 BLR02 L

YES(?,O(1))

We consider the following Problem:

  Strict Trs:
    {  filter(cons(X), 0(), M) -> cons(0())
     , filter(cons(X), s(N), M) -> cons(X)
     , sieve(cons(0())) -> cons(0())
     , sieve(cons(s(N))) -> cons(s(N))
     , nats(N) -> cons(N)
     , zprimes() -> sieve(nats(s(s(0()))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(1))

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

   safe(filter) = {2}, safe(cons) = {1}, safe(0) = {}, safe(s) = {1},
   safe(sieve) = {1}, safe(nats) = {1}, safe(zprimes) = {}

  and precedence

   zprimes > sieve, zprimes > nats .

  Following symbols are considered recursive:

   {}

  The recursion depth is 0 .

  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):

   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  filter(cons(; X), M; 0()) -> cons(; 0())
      , filter(cons(; X), M; s(; N)) -> cons(; X)
      , sieve(; cons(; 0())) -> cons(; 0())
      , sieve(; cons(; s(; N))) -> cons(; s(; N))
      , nats(; N) -> cons(; N)
      , zprimes() -> sieve(; nats(; s(; s(; 0()))))}
   Weak Trs  : {}

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

Problem Transformed CSR 04 Ex9 BLR02 L

LMPO

MPO

POP*

POP* (PS)

Small POP*

Small POP* (PS)