Problem Secret 06 TRS addList

LMPO

Execution Time (secs)
0.164
Answer
MAYBE
InputSecret 06 TRS addList
MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(cons(x, xs)) -> false()
     , isEmpty(nil()) -> true()
     , isZero(0()) -> true()
     , isZero(s(x)) -> false()
     , head(cons(x, xs)) -> x
     , tail(cons(x, xs)) -> xs
     , tail(nil()) -> nil()
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y, ys), x) -> cons(y, append(ys, x))
     , p(s(s(x))) -> s(p(s(x)))
     , p(s(0())) -> 0()
     , p(0()) -> 0()
     , inc(s(x)) -> s(inc(x))
     , inc(0()) -> s(0())
     , addLists(xs, ys, zs) ->
       if(isEmpty(xs),
          isEmpty(ys),
          isZero(head(xs)),
          tail(xs),
          tail(ys),
          cons(p(head(xs)), tail(xs)),
          cons(inc(head(ys)), tail(ys)),
          zs,
          append(zs, head(ys)))
     , if(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> zs
     , if(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs2, ys2, zs)
     , if(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs, ys, zs2)
     , addList(xs, ys) -> addLists(xs, ys, nil())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MPO

Execution Time (secs)
0.210
Answer
MAYBE
InputSecret 06 TRS addList
MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(cons(x, xs)) -> false()
     , isEmpty(nil()) -> true()
     , isZero(0()) -> true()
     , isZero(s(x)) -> false()
     , head(cons(x, xs)) -> x
     , tail(cons(x, xs)) -> xs
     , tail(nil()) -> nil()
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y, ys), x) -> cons(y, append(ys, x))
     , p(s(s(x))) -> s(p(s(x)))
     , p(s(0())) -> 0()
     , p(0()) -> 0()
     , inc(s(x)) -> s(inc(x))
     , inc(0()) -> s(0())
     , addLists(xs, ys, zs) ->
       if(isEmpty(xs),
          isEmpty(ys),
          isZero(head(xs)),
          tail(xs),
          tail(ys),
          cons(p(head(xs)), tail(xs)),
          cons(inc(head(ys)), tail(ys)),
          zs,
          append(zs, head(ys)))
     , if(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> zs
     , if(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs2, ys2, zs)
     , if(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs, ys, zs2)
     , addList(xs, ys) -> addLists(xs, ys, nil())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP*

Execution Time (secs)
0.281
Answer
MAYBE
InputSecret 06 TRS addList
MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(cons(x, xs)) -> false()
     , isEmpty(nil()) -> true()
     , isZero(0()) -> true()
     , isZero(s(x)) -> false()
     , head(cons(x, xs)) -> x
     , tail(cons(x, xs)) -> xs
     , tail(nil()) -> nil()
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y, ys), x) -> cons(y, append(ys, x))
     , p(s(s(x))) -> s(p(s(x)))
     , p(s(0())) -> 0()
     , p(0()) -> 0()
     , inc(s(x)) -> s(inc(x))
     , inc(0()) -> s(0())
     , addLists(xs, ys, zs) ->
       if(isEmpty(xs),
          isEmpty(ys),
          isZero(head(xs)),
          tail(xs),
          tail(ys),
          cons(p(head(xs)), tail(xs)),
          cons(inc(head(ys)), tail(ys)),
          zs,
          append(zs, head(ys)))
     , if(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> zs
     , if(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs2, ys2, zs)
     , if(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs, ys, zs2)
     , addList(xs, ys) -> addLists(xs, ys, nil())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP* (PS)

Execution Time (secs)
0.226
Answer
MAYBE
InputSecret 06 TRS addList
MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(cons(x, xs)) -> false()
     , isEmpty(nil()) -> true()
     , isZero(0()) -> true()
     , isZero(s(x)) -> false()
     , head(cons(x, xs)) -> x
     , tail(cons(x, xs)) -> xs
     , tail(nil()) -> nil()
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y, ys), x) -> cons(y, append(ys, x))
     , p(s(s(x))) -> s(p(s(x)))
     , p(s(0())) -> 0()
     , p(0()) -> 0()
     , inc(s(x)) -> s(inc(x))
     , inc(0()) -> s(0())
     , addLists(xs, ys, zs) ->
       if(isEmpty(xs),
          isEmpty(ys),
          isZero(head(xs)),
          tail(xs),
          tail(ys),
          cons(p(head(xs)), tail(xs)),
          cons(inc(head(ys)), tail(ys)),
          zs,
          append(zs, head(ys)))
     , if(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> zs
     , if(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs2, ys2, zs)
     , if(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs, ys, zs2)
     , addList(xs, ys) -> addLists(xs, ys, nil())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP*

Execution Time (secs)
0.184
Answer
MAYBE
InputSecret 06 TRS addList
MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(cons(x, xs)) -> false()
     , isEmpty(nil()) -> true()
     , isZero(0()) -> true()
     , isZero(s(x)) -> false()
     , head(cons(x, xs)) -> x
     , tail(cons(x, xs)) -> xs
     , tail(nil()) -> nil()
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y, ys), x) -> cons(y, append(ys, x))
     , p(s(s(x))) -> s(p(s(x)))
     , p(s(0())) -> 0()
     , p(0()) -> 0()
     , inc(s(x)) -> s(inc(x))
     , inc(0()) -> s(0())
     , addLists(xs, ys, zs) ->
       if(isEmpty(xs),
          isEmpty(ys),
          isZero(head(xs)),
          tail(xs),
          tail(ys),
          cons(p(head(xs)), tail(xs)),
          cons(inc(head(ys)), tail(ys)),
          zs,
          append(zs, head(ys)))
     , if(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> zs
     , if(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs2, ys2, zs)
     , if(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs, ys, zs2)
     , addList(xs, ys) -> addLists(xs, ys, nil())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP* (PS)

Execution Time (secs)
0.181
Answer
MAYBE
InputSecret 06 TRS addList
MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(cons(x, xs)) -> false()
     , isEmpty(nil()) -> true()
     , isZero(0()) -> true()
     , isZero(s(x)) -> false()
     , head(cons(x, xs)) -> x
     , tail(cons(x, xs)) -> xs
     , tail(nil()) -> nil()
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y, ys), x) -> cons(y, append(ys, x))
     , p(s(s(x))) -> s(p(s(x)))
     , p(s(0())) -> 0()
     , p(0()) -> 0()
     , inc(s(x)) -> s(inc(x))
     , inc(0()) -> s(0())
     , addLists(xs, ys, zs) ->
       if(isEmpty(xs),
          isEmpty(ys),
          isZero(head(xs)),
          tail(xs),
          tail(ys),
          cons(p(head(xs)), tail(xs)),
          cons(inc(head(ys)), tail(ys)),
          zs,
          append(zs, head(ys)))
     , if(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> zs
     , if(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs2, ys2, zs)
     , if(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs, ys, zs2)
     , addList(xs, ys) -> addLists(xs, ys, nil())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..