MAYBE 0.08/0.18 MAYBE 0.08/0.18 0.08/0.18 Problem: 0.08/0.18 isEmpty(empty()) -> true() 0.08/0.18 isEmpty(node(l,r)) -> false() 0.08/0.18 left(empty()) -> empty() 0.08/0.18 left(node(l,r)) -> l 0.08/0.18 right(empty()) -> empty() 0.08/0.18 right(node(l,r)) -> r 0.08/0.18 inc(0()) -> s(0()) 0.08/0.18 inc(s(x)) -> s(inc(x)) 0.08/0.18 count(n,x) -> 0.08/0.18 if(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),node(right(left(n)),right(n))),x,inc(x)) 0.08/0.18 if(true(),b,n,m,x,y) -> x 0.08/0.18 if(false(),false(),n,m,x,y) -> count(m,x) 0.08/0.18 if(false(),true(),n,m,x,y) -> count(n,y) 0.08/0.18 nrOfNodes(n) -> count(n,0()) 0.08/0.18 0.08/0.18 Proof: 0.08/0.18 Open 0.08/0.19 EOF