Problem CiME 04 list-sum-prod

MAYBE

We consider the following Problem:

  Strict Trs:
    {  +(x, 0()) -> x
     , +(0(), x) -> x
     , +(s(x), s(y)) -> s(s(+(x, y)))
     , *(x, 0()) -> 0()
     , *(0(), x) -> 0()
     , *(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
     , sum(nil()) -> 0()
     , sum(cons(x, l)) -> +(x, sum(l))
     , prod(nil()) -> s(0())
     , prod(cons(x, l)) -> *(x, prod(l))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

YES(?,PRIMREC)

We consider the following Problem:

  Strict Trs:
    {  +(x, 0()) -> x
     , +(0(), x) -> x
     , +(s(x), s(y)) -> s(s(+(x, y)))
     , *(x, 0()) -> 0()
     , *(0(), x) -> 0()
     , *(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
     , sum(nil()) -> 0()
     , sum(cons(x, l)) -> +(x, sum(l))
     , prod(nil()) -> s(0())
     , prod(cons(x, l)) -> *(x, prod(l))}
  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
  
   + > s, * > +, * > s, sum > +, nil > 0, nil > s, cons > *,
   cons > prod .

Hurray, we answered YES(?,PRIMREC)

MAYBE

We consider the following Problem:

  Strict Trs:
    {  +(x, 0()) -> x
     , +(0(), x) -> x
     , +(s(x), s(y)) -> s(s(+(x, y)))
     , *(x, 0()) -> 0()
     , *(0(), x) -> 0()
     , *(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
     , sum(nil()) -> 0()
     , sum(cons(x, l)) -> +(x, sum(l))
     , prod(nil()) -> s(0())
     , prod(cons(x, l)) -> *(x, prod(l))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  +(x, 0()) -> x
     , +(0(), x) -> x
     , +(s(x), s(y)) -> s(s(+(x, y)))
     , *(x, 0()) -> 0()
     , *(0(), x) -> 0()
     , *(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
     , sum(nil()) -> 0()
     , sum(cons(x, l)) -> +(x, sum(l))
     , prod(nil()) -> s(0())
     , prod(cons(x, l)) -> *(x, prod(l))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  +(x, 0()) -> x
     , +(0(), x) -> x
     , +(s(x), s(y)) -> s(s(+(x, y)))
     , *(x, 0()) -> 0()
     , *(0(), x) -> 0()
     , *(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
     , sum(nil()) -> 0()
     , sum(cons(x, l)) -> +(x, sum(l))
     , prod(nil()) -> s(0())
     , prod(cons(x, l)) -> *(x, prod(l))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  +(x, 0()) -> x
     , +(0(), x) -> x
     , +(s(x), s(y)) -> s(s(+(x, y)))
     , *(x, 0()) -> 0()
     , *(0(), x) -> 0()
     , *(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
     , sum(nil()) -> 0()
     , sum(cons(x, l)) -> +(x, sum(l))
     , prod(nil()) -> s(0())
     , prod(cons(x, l)) -> *(x, prod(l))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..