Problem Transformed CSR 04 Ex4 7 56 Bor03 Z

LMPO

Execution Time (secs)
0.043
Answer
MAYBE
InputTransformed CSR 04 Ex4 7 56 Bor03 Z
MAYBE

We consider the following Problem:

  Strict Trs:
    {  from(X) -> cons(X, n__from(s(X)))
     , after(0(), XS) -> XS
     , after(s(N), cons(X, XS)) -> after(N, activate(XS))
     , 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.058
Answer
MAYBE
InputTransformed CSR 04 Ex4 7 56 Bor03 Z
MAYBE

We consider the following Problem:

  Strict Trs:
    {  from(X) -> cons(X, n__from(s(X)))
     , after(0(), XS) -> XS
     , after(s(N), cons(X, XS)) -> after(N, activate(XS))
     , 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 Ex4 7 56 Bor03 Z
MAYBE

We consider the following Problem:

  Strict Trs:
    {  from(X) -> cons(X, n__from(s(X)))
     , after(0(), XS) -> XS
     , after(s(N), cons(X, XS)) -> after(N, activate(XS))
     , 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.048
Answer
YES(?,POLY)
InputTransformed CSR 04 Ex4 7 56 Bor03 Z
YES(?,POLY)

We consider the following Problem:

  Strict Trs:
    {  from(X) -> cons(X, n__from(s(X)))
     , after(0(), XS) -> XS
     , after(s(N), cons(X, XS)) -> after(N, activate(XS))
     , 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(after) = {2}, safe(0) = {},
   safe(activate) = {1}
  
  and precedence
  
   after > activate, activate > from .
  
  Following symbols are considered recursive:
  
   {after}
  
  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)))
      , after(0(); XS) -> XS
      , after(s(; N); cons(; X, XS)) -> after(N; activate(; XS))
      , 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.045
Answer
MAYBE
InputTransformed CSR 04 Ex4 7 56 Bor03 Z
MAYBE

We consider the following Problem:

  Strict Trs:
    {  from(X) -> cons(X, n__from(s(X)))
     , after(0(), XS) -> XS
     , after(s(N), cons(X, XS)) -> after(N, activate(XS))
     , 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.064
Answer
YES(?,O(n^1))
InputTransformed CSR 04 Ex4 7 56 Bor03 Z
YES(?,O(n^1))

We consider the following Problem:

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

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