Problem Der95 11

YES(?,ELEMENTARY)

We consider the following Problem:

  Strict Trs:
    {  D(t()) -> 1()
     , D(constant()) -> 0()
     , D(+(x, y)) -> +(D(x), D(y))
     , D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
     , D(-(x, y)) -> -(D(x), D(y))
     , D(minus(x)) -> minus(D(x))
     , D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2())))
     , D(ln(x)) -> div(D(x), x)
     , D(pow(x, y)) ->
       +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y)))}
  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(D) = {}, safe(t) = {}, safe(1) = {}, safe(constant) = {},
   safe(0) = {}, safe(+) = {1, 2}, safe(*) = {1, 2}, safe(-) = {1, 2},
   safe(minus) = {1}, safe(div) = {1, 2}, safe(pow) = {1, 2},
   safe(2) = {}, safe(ln) = {1}
  
  and precedence
  
   empty .
  
  Following symbols are considered recursive:
  
   {D}
  
  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:
     {  D(t();) -> 1()
      , D(constant();) -> 0()
      , D(+(; x, y);) -> +(; D(x;), D(y;))
      , D(*(; x, y);) -> +(; *(; y, D(x;)), *(; x, D(y;)))
      , D(-(; x, y);) -> -(; D(x;), D(y;))
      , D(minus(; x);) -> minus(; D(x;))
      , D(div(; x, y);) ->
        -(; div(; D(x;), y), div(; *(; x, D(y;)), pow(; y, 2())))
      , D(ln(; x);) -> div(; D(x;), x)
      , D(pow(; x, y);) ->
        +(; *(; *(; y, pow(; x, -(; y, 1()))), D(x;)),
            *(; *(; pow(; x, y), ln(; x)), D(y;)))}
   Weak Trs  : {}

Hurray, we answered YES(?,ELEMENTARY)

YES(?,PRIMREC)

We consider the following Problem:

  Strict Trs:
    {  D(t()) -> 1()
     , D(constant()) -> 0()
     , D(+(x, y)) -> +(D(x), D(y))
     , D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
     , D(-(x, y)) -> -(D(x), D(y))
     , D(minus(x)) -> minus(D(x))
     , D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2())))
     , D(ln(x)) -> div(D(x), x)
     , D(pow(x, y)) ->
       +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y)))}
  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
  
   D > 1, D > +, D > *, D > -, D > minus, D > div, D > pow, D > 2,
   D > ln, constant > 0 .

Hurray, we answered YES(?,PRIMREC)

MAYBE

We consider the following Problem:

  Strict Trs:
    {  D(t()) -> 1()
     , D(constant()) -> 0()
     , D(+(x, y)) -> +(D(x), D(y))
     , D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
     , D(-(x, y)) -> -(D(x), D(y))
     , D(minus(x)) -> minus(D(x))
     , D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2())))
     , D(ln(x)) -> div(D(x), x)
     , D(pow(x, y)) ->
       +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  D(t()) -> 1()
     , D(constant()) -> 0()
     , D(+(x, y)) -> +(D(x), D(y))
     , D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
     , D(-(x, y)) -> -(D(x), D(y))
     , D(minus(x)) -> minus(D(x))
     , D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2())))
     , D(ln(x)) -> div(D(x), x)
     , D(pow(x, y)) ->
       +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  D(t()) -> 1()
     , D(constant()) -> 0()
     , D(+(x, y)) -> +(D(x), D(y))
     , D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
     , D(-(x, y)) -> -(D(x), D(y))
     , D(minus(x)) -> minus(D(x))
     , D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2())))
     , D(ln(x)) -> div(D(x), x)
     , D(pow(x, y)) ->
       +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  D(t()) -> 1()
     , D(constant()) -> 0()
     , D(+(x, y)) -> +(D(x), D(y))
     , D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
     , D(-(x, y)) -> -(D(x), D(y))
     , D(minus(x)) -> minus(D(x))
     , D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2())))
     , D(ln(x)) -> div(D(x), x)
     , D(pow(x, y)) ->
       +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..