Problem Der95 18

YES(?,ELEMENTARY)

We consider the following Problem:

  Strict Trs: {*(x, +(y, z)) -> +(*(x, y), *(x, z))}
  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(*) = {}, safe(+) = {1, 2}
  
  and precedence
  
   empty .
  
  Following symbols are considered recursive:
  
   {*}
  
  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: {*(x, +(; y, z);) -> +(; *(x, y;), *(x, z;))}
   Weak Trs  : {}

Hurray, we answered YES(?,ELEMENTARY)

YES(?,PRIMREC)

We consider the following Problem:

  Strict Trs: {*(x, +(y, z)) -> +(*(x, y), *(x, z))}
  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
  
   * > + .

Hurray, we answered YES(?,PRIMREC)

MAYBE

We consider the following Problem:

  Strict Trs: {*(x, +(y, z)) -> +(*(x, y), *(x, z))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs: {*(x, +(y, z)) -> +(*(x, y), *(x, z))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs: {*(x, +(y, z)) -> +(*(x, y), *(x, z))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs: {*(x, +(y, z)) -> +(*(x, y), *(x, z))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..