MAYBE

Problem:
 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())

Proof:
 DP Processor:
  DPs:
   inc#(s(x)) -> inc#(x)
   count#(n,x) -> inc#(x)
   count#(n,x) -> right#(left(n))
   count#(n,x) -> left#(left(n))
   count#(n,x) -> right#(n)
   count#(n,x) -> left#(n)
   count#(n,x) -> isEmpty#(left(n))
   count#(n,x) -> isEmpty#(n)
   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#(false(),false(),n,m,x,y) -> count#(m,x)
   if#(false(),true(),n,m,x,y) -> count#(n,y)
   nrOfNodes#(n) -> count#(n,0())
  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())
  Open