LMPO

Execution Time (secs)	0.058
Answer	YES(?,ELEMENTARY)
Input	Transformed CSR 04 Ex25 Luc06 GM

YES(?,ELEMENTARY)

We consider the following Problem:

  Strict Trs:
    {  a__f(f(X)) -> a__c(f(g(f(X))))
     , a__c(X) -> d(X)
     , a__h(X) -> a__c(d(X))
     , mark(f(X)) -> a__f(mark(X))
     , mark(c(X)) -> a__c(X)
     , mark(h(X)) -> a__h(mark(X))
     , mark(g(X)) -> g(X)
     , mark(d(X)) -> d(X)
     , a__f(X) -> f(X)
     , a__c(X) -> c(X)
     , a__h(X) -> h(X)}
  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(a__f) = {1}, safe(f) = {1}, safe(a__c) = {1}, safe(g) = {1},
   safe(d) = {1}, safe(a__h) = {1}, safe(mark) = {}, safe(c) = {1},
   safe(h) = {1}

  and precedence

   a__f > a__c, a__h > a__c, mark > a__f, mark > a__c, mark > a__h .

  Following symbols are considered recursive:

   {a__f, a__c, a__h, mark}

  The recursion depth is 3 .

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

   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  a__f(; f(; X)) -> a__c(; f(; g(; f(; X))))
      , a__c(; X) -> d(; X)
      , a__h(; X) -> a__c(; d(; X))
      , mark(f(; X);) -> a__f(; mark(X;))
      , mark(c(; X);) -> a__c(; X)
      , mark(h(; X);) -> a__h(; mark(X;))
      , mark(g(; X);) -> g(; X)
      , mark(d(; X);) -> d(; X)
      , a__f(; X) -> f(; X)
      , a__c(; X) -> c(; X)
      , a__h(; X) -> h(; X)}
   Weak Trs  : {}

Hurray, we answered YES(?,ELEMENTARY)

MPO

Execution Time (secs)	0.136
Answer	YES(?,PRIMREC)
Input	Transformed CSR 04 Ex25 Luc06 GM

YES(?,PRIMREC)

We consider the following Problem:

  Strict Trs:
    {  a__f(f(X)) -> a__c(f(g(f(X))))
     , a__c(X) -> d(X)
     , a__h(X) -> a__c(d(X))
     , mark(f(X)) -> a__f(mark(X))
     , mark(c(X)) -> a__c(X)
     , mark(h(X)) -> a__h(mark(X))
     , mark(g(X)) -> g(X)
     , mark(d(X)) -> d(X)
     , a__f(X) -> f(X)
     , a__c(X) -> c(X)
     , a__h(X) -> h(X)}
  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

   a__f > f, a__f > a__c, a__f > g, a__c > d, a__c > c, a__h > a__c,
   a__h > d, a__h > h, mark > a__f, mark > a__c, mark > a__h .

Hurray, we answered YES(?,PRIMREC)

POP*

Execution Time (secs)	0.065
Answer	YES(?,POLY)
Input	Transformed CSR 04 Ex25 Luc06 GM

YES(?,POLY)

We consider the following Problem:

  Strict Trs:
    {  a__f(f(X)) -> a__c(f(g(f(X))))
     , a__c(X) -> d(X)
     , a__h(X) -> a__c(d(X))
     , mark(f(X)) -> a__f(mark(X))
     , mark(c(X)) -> a__c(X)
     , mark(h(X)) -> a__h(mark(X))
     , mark(g(X)) -> g(X)
     , mark(d(X)) -> d(X)
     , a__f(X) -> f(X)
     , a__c(X) -> c(X)
     , a__h(X) -> h(X)}
  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(a__f) = {1}, safe(f) = {1}, safe(a__c) = {1}, safe(g) = {1},
   safe(d) = {1}, safe(a__h) = {1}, safe(mark) = {}, safe(c) = {1},
   safe(h) = {1}

  and precedence

   a__f > a__c, a__h > a__c, mark > a__f, mark > a__c, mark > a__h .

  Following symbols are considered recursive:

   {a__f, a__c, a__h, mark}

  The recursion depth is 3 .

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

   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  a__f(; f(; X)) -> a__c(; f(; g(; f(; X))))
      , a__c(; X) -> d(; X)
      , a__h(; X) -> a__c(; d(; X))
      , mark(f(; X);) -> a__f(; mark(X;))
      , mark(c(; X);) -> a__c(; X)
      , mark(h(; X);) -> a__h(; mark(X;))
      , mark(g(; X);) -> g(; X)
      , mark(d(; X);) -> d(; X)
      , a__f(; X) -> f(; X)
      , a__c(; X) -> c(; X)
      , a__h(; X) -> h(; X)}
   Weak Trs  : {}

Hurray, we answered YES(?,POLY)

POP* (PS)

Execution Time (secs)	0.059
Answer	YES(?,POLY)
Input	Transformed CSR 04 Ex25 Luc06 GM

YES(?,POLY)

We consider the following Problem:

  Strict Trs:
    {  a__f(f(X)) -> a__c(f(g(f(X))))
     , a__c(X) -> d(X)
     , a__h(X) -> a__c(d(X))
     , mark(f(X)) -> a__f(mark(X))
     , mark(c(X)) -> a__c(X)
     , mark(h(X)) -> a__h(mark(X))
     , mark(g(X)) -> g(X)
     , mark(d(X)) -> d(X)
     , a__f(X) -> f(X)
     , a__c(X) -> c(X)
     , a__h(X) -> h(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(a__f) = {1}, safe(f) = {1}, safe(a__c) = {1}, safe(g) = {1},
   safe(d) = {1}, safe(a__h) = {1}, safe(mark) = {}, safe(c) = {1},
   safe(h) = {1}

  and precedence

   a__f > a__c, a__h > a__c, mark > a__f, mark > a__c, mark > a__h .

  Following symbols are considered recursive:

   {a__f, a__c, a__h, mark}

  The recursion depth is 3 .

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

   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  a__f(; f(; X)) -> a__c(; f(; g(; f(; X))))
      , a__c(; X) -> d(; X)
      , a__h(; X) -> a__c(; d(; X))
      , mark(f(; X);) -> a__f(; mark(X;))
      , mark(c(; X);) -> a__c(; X)
      , mark(h(; X);) -> a__h(; mark(X;))
      , mark(g(; X);) -> g(; X)
      , mark(d(; X);) -> d(; X)
      , a__f(; X) -> f(; X)
      , a__c(; X) -> c(; X)
      , a__h(; X) -> h(; X)}
   Weak Trs  : {}

Hurray, we answered YES(?,POLY)

Small POP*

Execution Time (secs)	0.194
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex25 Luc06 GM

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  a__f(f(X)) -> a__c(f(g(f(X))))
     , a__c(X) -> d(X)
     , a__h(X) -> a__c(d(X))
     , mark(f(X)) -> a__f(mark(X))
     , mark(c(X)) -> a__c(X)
     , mark(h(X)) -> a__h(mark(X))
     , mark(g(X)) -> g(X)
     , mark(d(X)) -> d(X)
     , a__f(X) -> f(X)
     , a__c(X) -> c(X)
     , a__h(X) -> h(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,
                             Nat 1-bounded) as induced by the safe mapping

   safe(a__f) = {1}, safe(f) = {1}, safe(a__c) = {1}, safe(g) = {1},
   safe(d) = {1}, safe(a__h) = {1}, safe(mark) = {}, safe(c) = {1},
   safe(h) = {1}

  and precedence

   a__f > a__c, a__h > a__c, mark > a__f, mark > a__c, mark > a__h .

  Following symbols are considered recursive:

   {mark}

  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:
     {  a__f(; f(; X)) -> a__c(; f(; g(; f(; X))))
      , a__c(; X) -> d(; X)
      , a__h(; X) -> a__c(; d(; X))
      , mark(f(; X);) -> a__f(; mark(X;))
      , mark(c(; X);) -> a__c(; X)
      , mark(h(; X);) -> a__h(; mark(X;))
      , mark(g(; X);) -> g(; X)
      , mark(d(; X);) -> d(; X)
      , a__f(; X) -> f(; X)
      , a__c(; X) -> c(; X)
      , a__h(; X) -> h(; X)}
   Weak Trs  : {}

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

Small POP* (PS)

Execution Time (secs)	0.112
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex25 Luc06 GM

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  a__f(f(X)) -> a__c(f(g(f(X))))
     , a__c(X) -> d(X)
     , a__h(X) -> a__c(d(X))
     , mark(f(X)) -> a__f(mark(X))
     , mark(c(X)) -> a__c(X)
     , mark(h(X)) -> a__h(mark(X))
     , mark(g(X)) -> g(X)
     , mark(d(X)) -> d(X)
     , a__f(X) -> f(X)
     , a__c(X) -> c(X)
     , a__h(X) -> h(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,
                             Nat 1-bounded) as induced by the safe mapping

   safe(a__f) = {1}, safe(f) = {1}, safe(a__c) = {1}, safe(g) = {1},
   safe(d) = {1}, safe(a__h) = {1}, safe(mark) = {}, safe(c) = {1},
   safe(h) = {1}

  and precedence

   a__f > a__c, a__h > a__c, mark > a__f, mark > a__c, mark > a__h .

  Following symbols are considered recursive:

   {mark}

  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:
     {  a__f(; f(; X)) -> a__c(; f(; g(; f(; X))))
      , a__c(; X) -> d(; X)
      , a__h(; X) -> a__c(; d(; X))
      , mark(f(; X);) -> a__f(; mark(X;))
      , mark(c(; X);) -> a__c(; X)
      , mark(h(; X);) -> a__h(; mark(X;))
      , mark(g(; X);) -> g(; X)
      , mark(d(; X);) -> d(; X)
      , a__f(; X) -> f(; X)
      , a__c(; X) -> c(; X)
      , a__h(; X) -> h(; X)}
   Weak Trs  : {}

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

Problem Transformed CSR 04 Ex25 Luc06 GM

LMPO

MPO

POP*

POP* (PS)

Small POP*

Small POP* (PS)