Problem Secret 06 TRS toList

MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(empty()) -> true()
     , isEmpty(node(l, x, r)) -> false()
     , left(empty()) -> empty()
     , left(node(l, x, r)) -> l
     , right(empty()) -> empty()
     , right(node(l, x, r)) -> r
     , elem(node(l, x, r)) -> x
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y(), ys), x) -> cons(y(), append(ys, x))
     , listify(n, xs) ->
       if(isEmpty(n),
          isEmpty(left(n)),
          right(n),
          node(left(left(n)),
               elem(left(n)),
               node(right(left(n)), elem(n), right(n))),
          xs,
          append(xs, n))
     , if(true(), b, n, m, xs, ys) -> xs
     , if(false(), false(), n, m, xs, ys) -> listify(m, xs)
     , if(false(), true(), n, m, xs, ys) -> listify(n, ys)
     , toList(n) -> listify(n, nil())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(empty()) -> true()
     , isEmpty(node(l, x, r)) -> false()
     , left(empty()) -> empty()
     , left(node(l, x, r)) -> l
     , right(empty()) -> empty()
     , right(node(l, x, r)) -> r
     , elem(node(l, x, r)) -> x
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y(), ys), x) -> cons(y(), append(ys, x))
     , listify(n, xs) ->
       if(isEmpty(n),
          isEmpty(left(n)),
          right(n),
          node(left(left(n)),
               elem(left(n)),
               node(right(left(n)), elem(n), right(n))),
          xs,
          append(xs, n))
     , if(true(), b, n, m, xs, ys) -> xs
     , if(false(), false(), n, m, xs, ys) -> listify(m, xs)
     , if(false(), true(), n, m, xs, ys) -> listify(n, ys)
     , toList(n) -> listify(n, nil())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(empty()) -> true()
     , isEmpty(node(l, x, r)) -> false()
     , left(empty()) -> empty()
     , left(node(l, x, r)) -> l
     , right(empty()) -> empty()
     , right(node(l, x, r)) -> r
     , elem(node(l, x, r)) -> x
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y(), ys), x) -> cons(y(), append(ys, x))
     , listify(n, xs) ->
       if(isEmpty(n),
          isEmpty(left(n)),
          right(n),
          node(left(left(n)),
               elem(left(n)),
               node(right(left(n)), elem(n), right(n))),
          xs,
          append(xs, n))
     , if(true(), b, n, m, xs, ys) -> xs
     , if(false(), false(), n, m, xs, ys) -> listify(m, xs)
     , if(false(), true(), n, m, xs, ys) -> listify(n, ys)
     , toList(n) -> listify(n, nil())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(empty()) -> true()
     , isEmpty(node(l, x, r)) -> false()
     , left(empty()) -> empty()
     , left(node(l, x, r)) -> l
     , right(empty()) -> empty()
     , right(node(l, x, r)) -> r
     , elem(node(l, x, r)) -> x
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y(), ys), x) -> cons(y(), append(ys, x))
     , listify(n, xs) ->
       if(isEmpty(n),
          isEmpty(left(n)),
          right(n),
          node(left(left(n)),
               elem(left(n)),
               node(right(left(n)), elem(n), right(n))),
          xs,
          append(xs, n))
     , if(true(), b, n, m, xs, ys) -> xs
     , if(false(), false(), n, m, xs, ys) -> listify(m, xs)
     , if(false(), true(), n, m, xs, ys) -> listify(n, ys)
     , toList(n) -> listify(n, nil())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(empty()) -> true()
     , isEmpty(node(l, x, r)) -> false()
     , left(empty()) -> empty()
     , left(node(l, x, r)) -> l
     , right(empty()) -> empty()
     , right(node(l, x, r)) -> r
     , elem(node(l, x, r)) -> x
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y(), ys), x) -> cons(y(), append(ys, x))
     , listify(n, xs) ->
       if(isEmpty(n),
          isEmpty(left(n)),
          right(n),
          node(left(left(n)),
               elem(left(n)),
               node(right(left(n)), elem(n), right(n))),
          xs,
          append(xs, n))
     , if(true(), b, n, m, xs, ys) -> xs
     , if(false(), false(), n, m, xs, ys) -> listify(m, xs)
     , if(false(), true(), n, m, xs, ys) -> listify(n, ys)
     , toList(n) -> listify(n, nil())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(empty()) -> true()
     , isEmpty(node(l, x, r)) -> false()
     , left(empty()) -> empty()
     , left(node(l, x, r)) -> l
     , right(empty()) -> empty()
     , right(node(l, x, r)) -> r
     , elem(node(l, x, r)) -> x
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y(), ys), x) -> cons(y(), append(ys, x))
     , listify(n, xs) ->
       if(isEmpty(n),
          isEmpty(left(n)),
          right(n),
          node(left(left(n)),
               elem(left(n)),
               node(right(left(n)), elem(n), right(n))),
          xs,
          append(xs, n))
     , if(true(), b, n, m, xs, ys) -> xs
     , if(false(), false(), n, m, xs, ys) -> listify(m, xs)
     , if(false(), true(), n, m, xs, ys) -> listify(n, ys)
     , toList(n) -> listify(n, nil())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..