Problem Transformed CSR 04 Ex3 12 Luc96a Z

LMPO

Execution Time (secs)
0.034
Answer
MAYBE
InputTransformed CSR 04 Ex3 12 Luc96a Z
MAYBE

We consider the following Problem:

  Strict Trs:
    {  from(X) -> cons(X, n__from(s(X)))
     , sel(0(), cons(X, Y)) -> X
     , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
     , from(X) -> n__from(X)
     , activate(n__from(X)) -> from(X)
     , activate(X) -> X}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MPO

Execution Time (secs)
0.042
Answer
MAYBE
InputTransformed CSR 04 Ex3 12 Luc96a Z
MAYBE

We consider the following Problem:

  Strict Trs:
    {  from(X) -> cons(X, n__from(s(X)))
     , sel(0(), cons(X, Y)) -> X
     , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
     , from(X) -> n__from(X)
     , activate(n__from(X)) -> from(X)
     , activate(X) -> X}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP*

Execution Time (secs)
0.043
Answer
MAYBE
InputTransformed CSR 04 Ex3 12 Luc96a Z
MAYBE

We consider the following Problem:

  Strict Trs:
    {  from(X) -> cons(X, n__from(s(X)))
     , sel(0(), cons(X, Y)) -> X
     , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
     , from(X) -> n__from(X)
     , activate(n__from(X)) -> from(X)
     , activate(X) -> X}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP* (PS)

Execution Time (secs)
0.084
Answer
YES(?,POLY)
InputTransformed CSR 04 Ex3 12 Luc96a Z
YES(?,POLY)

We consider the following Problem:

  Strict Trs:
    {  from(X) -> cons(X, n__from(s(X)))
     , sel(0(), cons(X, Y)) -> X
     , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
     , from(X) -> n__from(X)
     , activate(n__from(X)) -> from(X)
     , activate(X) -> X}
  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(from) = {1}, safe(cons) = {1, 2}, safe(n__from) = {1},
   safe(s) = {1}, safe(sel) = {2}, safe(0) = {}, safe(activate) = {1}
  
  and precedence
  
   sel > activate, activate > from .
  
  Following symbols are considered recursive:
  
   {sel}
  
  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:
     {  from(; X) -> cons(; X, n__from(; s(; X)))
      , sel(0(); cons(; X, Y)) -> X
      , sel(s(; X); cons(; Y, Z)) -> sel(X; activate(; Z))
      , from(; X) -> n__from(; X)
      , activate(; n__from(; X)) -> from(; X)
      , activate(; X) -> X}
   Weak Trs  : {}

Hurray, we answered YES(?,POLY)

Small POP*

Execution Time (secs)
0.021
Answer
MAYBE
InputTransformed CSR 04 Ex3 12 Luc96a Z
MAYBE

We consider the following Problem:

  Strict Trs:
    {  from(X) -> cons(X, n__from(s(X)))
     , sel(0(), cons(X, Y)) -> X
     , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
     , from(X) -> n__from(X)
     , activate(n__from(X)) -> from(X)
     , activate(X) -> X}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP* (PS)

Execution Time (secs)
0.081
Answer
YES(?,O(n^1))
InputTransformed CSR 04 Ex3 12 Luc96a Z
YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  from(X) -> cons(X, n__from(s(X)))
     , sel(0(), cons(X, Y)) -> X
     , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
     , from(X) -> n__from(X)
     , activate(n__from(X)) -> from(X)
     , activate(X) -> X}
  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(from) = {1}, safe(cons) = {1, 2}, safe(n__from) = {1},
   safe(s) = {1}, safe(sel) = {2}, safe(0) = {}, safe(activate) = {1}
  
  and precedence
  
   sel > activate, activate > from .
  
  Following symbols are considered recursive:
  
   {sel}
  
  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:
     {  from(; X) -> cons(; X, n__from(; s(; X)))
      , sel(0(); cons(; X, Y)) -> X
      , sel(s(; X); cons(; Y, Z)) -> sel(X; activate(; Z))
      , from(; X) -> n__from(; X)
      , activate(; n__from(; X)) -> from(; X)
      , activate(; X) -> X}
   Weak Trs  : {}

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