Problem Secret 06 TRS nrOfNodes

MAYBE

We consider the following Problem:

  Strict Trs:
    {  isEmpty(empty()) -> true()
     , isEmpty(node(l, r)) -> false()
     , left(empty()) -> empty()
     , left(node(l, r)) -> l
     , right(empty()) -> empty()
     , right(node(l, r)) -> r
     , inc(0()) -> s(0())
     , inc(s(x)) -> s(inc(x))
     , count(n, x) ->
       if(isEmpty(n),
          isEmpty(left(n)),
          right(n),
          node(left(left(n)), node(right(left(n)), right(n))),
          x,
          inc(x))
     , if(true(), b, n, m, x, y) -> x
     , if(false(), false(), n, m, x, y) -> count(m, x)
     , if(false(), true(), n, m, x, y) -> count(n, y)
     , nrOfNodes(n) -> count(n, 0())}
  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, r)) -> false()
     , left(empty()) -> empty()
     , left(node(l, r)) -> l
     , right(empty()) -> empty()
     , right(node(l, r)) -> r
     , inc(0()) -> s(0())
     , inc(s(x)) -> s(inc(x))
     , count(n, x) ->
       if(isEmpty(n),
          isEmpty(left(n)),
          right(n),
          node(left(left(n)), node(right(left(n)), right(n))),
          x,
          inc(x))
     , if(true(), b, n, m, x, y) -> x
     , if(false(), false(), n, m, x, y) -> count(m, x)
     , if(false(), true(), n, m, x, y) -> count(n, y)
     , nrOfNodes(n) -> count(n, 0())}
  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, r)) -> false()
     , left(empty()) -> empty()
     , left(node(l, r)) -> l
     , right(empty()) -> empty()
     , right(node(l, r)) -> r
     , inc(0()) -> s(0())
     , inc(s(x)) -> s(inc(x))
     , count(n, x) ->
       if(isEmpty(n),
          isEmpty(left(n)),
          right(n),
          node(left(left(n)), node(right(left(n)), right(n))),
          x,
          inc(x))
     , if(true(), b, n, m, x, y) -> x
     , if(false(), false(), n, m, x, y) -> count(m, x)
     , if(false(), true(), n, m, x, y) -> count(n, y)
     , nrOfNodes(n) -> count(n, 0())}
  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, r)) -> false()
     , left(empty()) -> empty()
     , left(node(l, r)) -> l
     , right(empty()) -> empty()
     , right(node(l, r)) -> r
     , inc(0()) -> s(0())
     , inc(s(x)) -> s(inc(x))
     , count(n, x) ->
       if(isEmpty(n),
          isEmpty(left(n)),
          right(n),
          node(left(left(n)), node(right(left(n)), right(n))),
          x,
          inc(x))
     , if(true(), b, n, m, x, y) -> x
     , if(false(), false(), n, m, x, y) -> count(m, x)
     , if(false(), true(), n, m, x, y) -> count(n, y)
     , nrOfNodes(n) -> count(n, 0())}
  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, r)) -> false()
     , left(empty()) -> empty()
     , left(node(l, r)) -> l
     , right(empty()) -> empty()
     , right(node(l, r)) -> r
     , inc(0()) -> s(0())
     , inc(s(x)) -> s(inc(x))
     , count(n, x) ->
       if(isEmpty(n),
          isEmpty(left(n)),
          right(n),
          node(left(left(n)), node(right(left(n)), right(n))),
          x,
          inc(x))
     , if(true(), b, n, m, x, y) -> x
     , if(false(), false(), n, m, x, y) -> count(m, x)
     , if(false(), true(), n, m, x, y) -> count(n, y)
     , nrOfNodes(n) -> count(n, 0())}
  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, r)) -> false()
     , left(empty()) -> empty()
     , left(node(l, r)) -> l
     , right(empty()) -> empty()
     , right(node(l, r)) -> r
     , inc(0()) -> s(0())
     , inc(s(x)) -> s(inc(x))
     , count(n, x) ->
       if(isEmpty(n),
          isEmpty(left(n)),
          right(n),
          node(left(left(n)), node(right(left(n)), right(n))),
          x,
          inc(x))
     , if(true(), b, n, m, x, y) -> x
     , if(false(), false(), n, m, x, y) -> count(m, x)
     , if(false(), true(), n, m, x, y) -> count(n, y)
     , nrOfNodes(n) -> count(n, 0())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..