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())
  TDG 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())
   graph:
    nrOfNodes#(n) -> count#(n,0()) ->
    count#(n,x) ->
    if#(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),node(right(left(n)),right(n))),
        x,inc(x))
    nrOfNodes#(n) -> count#(n,0()) -> count#(n,x) -> isEmpty#(n)
    nrOfNodes#(n) -> count#(n,0()) ->
    count#(n,x) -> isEmpty#(left(n))
    nrOfNodes#(n) -> count#(n,0()) -> count#(n,x) -> left#(n)
    nrOfNodes#(n) -> count#(n,0()) -> count#(n,x) -> right#(n)
    nrOfNodes#(n) -> count#(n,0()) -> count#(n,x) -> left#(left(n))
    nrOfNodes#(n) -> count#(n,0()) -> count#(n,x) -> right#(left(n))
    nrOfNodes#(n) -> count#(n,0()) ->
    count#(n,x) -> inc#(x)
    if#(false(),false(),n,m,x,y) -> count#(m,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#(false(),false(),n,m,x,y) -> count#(m,x) ->
    count#(n,x) -> isEmpty#(n)
    if#(false(),false(),n,m,x,y) -> count#(m,x) ->
    count#(n,x) -> isEmpty#(left(n))
    if#(false(),false(),n,m,x,y) -> count#(m,x) ->
    count#(n,x) -> left#(n)
    if#(false(),false(),n,m,x,y) -> count#(m,x) ->
    count#(n,x) -> right#(n)
    if#(false(),false(),n,m,x,y) -> count#(m,x) ->
    count#(n,x) -> left#(left(n))
    if#(false(),false(),n,m,x,y) -> count#(m,x) ->
    count#(n,x) -> right#(left(n))
    if#(false(),false(),n,m,x,y) -> count#(m,x) ->
    count#(n,x) -> inc#(x)
    if#(false(),true(),n,m,x,y) -> count#(n,y) ->
    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(),true(),n,m,x,y) -> count#(n,y) ->
    count#(n,x) -> isEmpty#(n)
    if#(false(),true(),n,m,x,y) -> count#(n,y) ->
    count#(n,x) -> isEmpty#(left(n))
    if#(false(),true(),n,m,x,y) -> count#(n,y) ->
    count#(n,x) -> left#(n)
    if#(false(),true(),n,m,x,y) -> count#(n,y) ->
    count#(n,x) -> right#(n)
    if#(false(),true(),n,m,x,y) -> count#(n,y) ->
    count#(n,x) -> left#(left(n))
    if#(false(),true(),n,m,x,y) -> count#(n,y) ->
    count#(n,x) -> right#(left(n))
    if#(false(),true(),n,m,x,y) -> count#(n,y) ->
    count#(n,x) -> 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#(false(),true(),n,m,x,y) -> count#(n,y)
    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)
    count#(n,x) -> inc#(x) -> inc#(s(x)) -> inc#(x)
    inc#(s(x)) -> inc#(x) -> inc#(s(x)) -> inc#(x)
   SCC Processor:
    #sccs: 2
    #rules: 4
    #arcs: 28/144
    DPs:
     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)
    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
    
    DPs:
     inc#(s(x)) -> inc#(x)
    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())
    Subterm Criterion Processor:
     simple projection:
      pi(inc#) = 0
     problem:
      DPs:
       
      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())
     Qed