MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: 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) if(true(),b,n,m,x,y) -> x inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(empty()) -> true() isEmpty(node(l,r)) -> false() left(empty()) -> empty() left(node(l,r)) -> l nrOfNodes(n) -> count(n,0()) right(empty()) -> empty() right(node(l,r)) -> r - Signature: {count/2,if/6,inc/1,isEmpty/1,left/1,nrOfNodes/1,right/1} / {0/0,empty/0,false/0,node/2,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {count,if,inc,isEmpty,left,nrOfNodes ,right} and constructors {0,empty,false,node,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,isEmpty#(n) ,isEmpty#(left(n)) ,left#(n) ,right#(n) ,left#(left(n)) ,left#(n) ,right#(left(n)) ,left#(n) ,right#(n) ,inc#(x)) if#(false(),false(),n,m,x,y) -> c_2(count#(m,x)) if#(false(),true(),n,m,x,y) -> c_3(count#(n,y)) if#(true(),b,n,m,x,y) -> c_4() inc#(0()) -> c_5() inc#(s(x)) -> c_6(inc#(x)) isEmpty#(empty()) -> c_7() isEmpty#(node(l,r)) -> c_8() left#(empty()) -> c_9() left#(node(l,r)) -> c_10() nrOfNodes#(n) -> c_11(count#(n,0())) right#(empty()) -> c_12() right#(node(l,r)) -> c_13() Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,isEmpty#(n) ,isEmpty#(left(n)) ,left#(n) ,right#(n) ,left#(left(n)) ,left#(n) ,right#(left(n)) ,left#(n) ,right#(n) ,inc#(x)) if#(false(),false(),n,m,x,y) -> c_2(count#(m,x)) if#(false(),true(),n,m,x,y) -> c_3(count#(n,y)) if#(true(),b,n,m,x,y) -> c_4() inc#(0()) -> c_5() inc#(s(x)) -> c_6(inc#(x)) isEmpty#(empty()) -> c_7() isEmpty#(node(l,r)) -> c_8() left#(empty()) -> c_9() left#(node(l,r)) -> c_10() nrOfNodes#(n) -> c_11(count#(n,0())) right#(empty()) -> c_12() right#(node(l,r)) -> c_13() - Weak TRS: 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) if(true(),b,n,m,x,y) -> x inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(empty()) -> true() isEmpty(node(l,r)) -> false() left(empty()) -> empty() left(node(l,r)) -> l nrOfNodes(n) -> count(n,0()) right(empty()) -> empty() right(node(l,r)) -> r - Signature: {count/2,if/6,inc/1,isEmpty/1,left/1,nrOfNodes/1,right/1,count#/2,if#/6,inc#/1,isEmpty#/1,left#/1 ,nrOfNodes#/1,right#/1} / {0/0,empty/0,false/0,node/2,s/1,true/0,c_1/11,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0 ,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {count#,if#,inc#,isEmpty#,left#,nrOfNodes# ,right#} and constructors {0,empty,false,node,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(empty()) -> true() isEmpty(node(l,r)) -> false() left(empty()) -> empty() left(node(l,r)) -> l right(empty()) -> empty() right(node(l,r)) -> r count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,isEmpty#(n) ,isEmpty#(left(n)) ,left#(n) ,right#(n) ,left#(left(n)) ,left#(n) ,right#(left(n)) ,left#(n) ,right#(n) ,inc#(x)) if#(false(),false(),n,m,x,y) -> c_2(count#(m,x)) if#(false(),true(),n,m,x,y) -> c_3(count#(n,y)) if#(true(),b,n,m,x,y) -> c_4() inc#(0()) -> c_5() inc#(s(x)) -> c_6(inc#(x)) isEmpty#(empty()) -> c_7() isEmpty#(node(l,r)) -> c_8() left#(empty()) -> c_9() left#(node(l,r)) -> c_10() nrOfNodes#(n) -> c_11(count#(n,0())) right#(empty()) -> c_12() right#(node(l,r)) -> c_13() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,isEmpty#(n) ,isEmpty#(left(n)) ,left#(n) ,right#(n) ,left#(left(n)) ,left#(n) ,right#(left(n)) ,left#(n) ,right#(n) ,inc#(x)) if#(false(),false(),n,m,x,y) -> c_2(count#(m,x)) if#(false(),true(),n,m,x,y) -> c_3(count#(n,y)) if#(true(),b,n,m,x,y) -> c_4() inc#(0()) -> c_5() inc#(s(x)) -> c_6(inc#(x)) isEmpty#(empty()) -> c_7() isEmpty#(node(l,r)) -> c_8() left#(empty()) -> c_9() left#(node(l,r)) -> c_10() nrOfNodes#(n) -> c_11(count#(n,0())) right#(empty()) -> c_12() right#(node(l,r)) -> c_13() - Weak TRS: inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(empty()) -> true() isEmpty(node(l,r)) -> false() left(empty()) -> empty() left(node(l,r)) -> l right(empty()) -> empty() right(node(l,r)) -> r - Signature: {count/2,if/6,inc/1,isEmpty/1,left/1,nrOfNodes/1,right/1,count#/2,if#/6,inc#/1,isEmpty#/1,left#/1 ,nrOfNodes#/1,right#/1} / {0/0,empty/0,false/0,node/2,s/1,true/0,c_1/11,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0 ,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {count#,if#,inc#,isEmpty#,left#,nrOfNodes# ,right#} and constructors {0,empty,false,node,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {4,5,7,8,9,10,12,13} by application of Pre({4,5,7,8,9,10,12,13}) = {1,6}. Here rules are labelled as follows: 1: count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,isEmpty#(n) ,isEmpty#(left(n)) ,left#(n) ,right#(n) ,left#(left(n)) ,left#(n) ,right#(left(n)) ,left#(n) ,right#(n) ,inc#(x)) 2: if#(false(),false(),n,m,x,y) -> c_2(count#(m,x)) 3: if#(false(),true(),n,m,x,y) -> c_3(count#(n,y)) 4: if#(true(),b,n,m,x,y) -> c_4() 5: inc#(0()) -> c_5() 6: inc#(s(x)) -> c_6(inc#(x)) 7: isEmpty#(empty()) -> c_7() 8: isEmpty#(node(l,r)) -> c_8() 9: left#(empty()) -> c_9() 10: left#(node(l,r)) -> c_10() 11: nrOfNodes#(n) -> c_11(count#(n,0())) 12: right#(empty()) -> c_12() 13: right#(node(l,r)) -> c_13() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,isEmpty#(n) ,isEmpty#(left(n)) ,left#(n) ,right#(n) ,left#(left(n)) ,left#(n) ,right#(left(n)) ,left#(n) ,right#(n) ,inc#(x)) if#(false(),false(),n,m,x,y) -> c_2(count#(m,x)) if#(false(),true(),n,m,x,y) -> c_3(count#(n,y)) inc#(s(x)) -> c_6(inc#(x)) nrOfNodes#(n) -> c_11(count#(n,0())) - Weak DPs: if#(true(),b,n,m,x,y) -> c_4() inc#(0()) -> c_5() isEmpty#(empty()) -> c_7() isEmpty#(node(l,r)) -> c_8() left#(empty()) -> c_9() left#(node(l,r)) -> c_10() right#(empty()) -> c_12() right#(node(l,r)) -> c_13() - Weak TRS: inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(empty()) -> true() isEmpty(node(l,r)) -> false() left(empty()) -> empty() left(node(l,r)) -> l right(empty()) -> empty() right(node(l,r)) -> r - Signature: {count/2,if/6,inc/1,isEmpty/1,left/1,nrOfNodes/1,right/1,count#/2,if#/6,inc#/1,isEmpty#/1,left#/1 ,nrOfNodes#/1,right#/1} / {0/0,empty/0,false/0,node/2,s/1,true/0,c_1/11,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0 ,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {count#,if#,inc#,isEmpty#,left#,nrOfNodes# ,right#} and constructors {0,empty,false,node,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,isEmpty#(n) ,isEmpty#(left(n)) ,left#(n) ,right#(n) ,left#(left(n)) ,left#(n) ,right#(left(n)) ,left#(n) ,right#(n) ,inc#(x)) -->_11 inc#(s(x)) -> c_6(inc#(x)):4 -->_1 if#(false(),true(),n,m,x,y) -> c_3(count#(n,y)):3 -->_1 if#(false(),false(),n,m,x,y) -> c_2(count#(m,x)):2 -->_10 right#(node(l,r)) -> c_13():13 -->_8 right#(node(l,r)) -> c_13():13 -->_5 right#(node(l,r)) -> c_13():13 -->_10 right#(empty()) -> c_12():12 -->_8 right#(empty()) -> c_12():12 -->_5 right#(empty()) -> c_12():12 -->_9 left#(node(l,r)) -> c_10():11 -->_7 left#(node(l,r)) -> c_10():11 -->_6 left#(node(l,r)) -> c_10():11 -->_4 left#(node(l,r)) -> c_10():11 -->_9 left#(empty()) -> c_9():10 -->_7 left#(empty()) -> c_9():10 -->_6 left#(empty()) -> c_9():10 -->_4 left#(empty()) -> c_9():10 -->_3 isEmpty#(node(l,r)) -> c_8():9 -->_2 isEmpty#(node(l,r)) -> c_8():9 -->_3 isEmpty#(empty()) -> c_7():8 -->_2 isEmpty#(empty()) -> c_7():8 -->_11 inc#(0()) -> c_5():7 -->_1 if#(true(),b,n,m,x,y) -> c_4():6 2:S:if#(false(),false(),n,m,x,y) -> c_2(count#(m,x)) -->_1 count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,isEmpty#(n) ,isEmpty#(left(n)) ,left#(n) ,right#(n) ,left#(left(n)) ,left#(n) ,right#(left(n)) ,left#(n) ,right#(n) ,inc#(x)):1 3:S:if#(false(),true(),n,m,x,y) -> c_3(count#(n,y)) -->_1 count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,isEmpty#(n) ,isEmpty#(left(n)) ,left#(n) ,right#(n) ,left#(left(n)) ,left#(n) ,right#(left(n)) ,left#(n) ,right#(n) ,inc#(x)):1 4:S:inc#(s(x)) -> c_6(inc#(x)) -->_1 inc#(0()) -> c_5():7 -->_1 inc#(s(x)) -> c_6(inc#(x)):4 5:S:nrOfNodes#(n) -> c_11(count#(n,0())) -->_1 count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,isEmpty#(n) ,isEmpty#(left(n)) ,left#(n) ,right#(n) ,left#(left(n)) ,left#(n) ,right#(left(n)) ,left#(n) ,right#(n) ,inc#(x)):1 6:W:if#(true(),b,n,m,x,y) -> c_4() 7:W:inc#(0()) -> c_5() 8:W:isEmpty#(empty()) -> c_7() 9:W:isEmpty#(node(l,r)) -> c_8() 10:W:left#(empty()) -> c_9() 11:W:left#(node(l,r)) -> c_10() 12:W:right#(empty()) -> c_12() 13:W:right#(node(l,r)) -> c_13() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: if#(true(),b,n,m,x,y) -> c_4() 8: isEmpty#(empty()) -> c_7() 9: isEmpty#(node(l,r)) -> c_8() 10: left#(empty()) -> c_9() 11: left#(node(l,r)) -> c_10() 12: right#(empty()) -> c_12() 13: right#(node(l,r)) -> c_13() 7: inc#(0()) -> c_5() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,isEmpty#(n) ,isEmpty#(left(n)) ,left#(n) ,right#(n) ,left#(left(n)) ,left#(n) ,right#(left(n)) ,left#(n) ,right#(n) ,inc#(x)) if#(false(),false(),n,m,x,y) -> c_2(count#(m,x)) if#(false(),true(),n,m,x,y) -> c_3(count#(n,y)) inc#(s(x)) -> c_6(inc#(x)) nrOfNodes#(n) -> c_11(count#(n,0())) - Weak TRS: inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(empty()) -> true() isEmpty(node(l,r)) -> false() left(empty()) -> empty() left(node(l,r)) -> l right(empty()) -> empty() right(node(l,r)) -> r - Signature: {count/2,if/6,inc/1,isEmpty/1,left/1,nrOfNodes/1,right/1,count#/2,if#/6,inc#/1,isEmpty#/1,left#/1 ,nrOfNodes#/1,right#/1} / {0/0,empty/0,false/0,node/2,s/1,true/0,c_1/11,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0 ,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {count#,if#,inc#,isEmpty#,left#,nrOfNodes# ,right#} and constructors {0,empty,false,node,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,isEmpty#(n) ,isEmpty#(left(n)) ,left#(n) ,right#(n) ,left#(left(n)) ,left#(n) ,right#(left(n)) ,left#(n) ,right#(n) ,inc#(x)) -->_11 inc#(s(x)) -> c_6(inc#(x)):4 -->_1 if#(false(),true(),n,m,x,y) -> c_3(count#(n,y)):3 -->_1 if#(false(),false(),n,m,x,y) -> c_2(count#(m,x)):2 2:S:if#(false(),false(),n,m,x,y) -> c_2(count#(m,x)) -->_1 count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,isEmpty#(n) ,isEmpty#(left(n)) ,left#(n) ,right#(n) ,left#(left(n)) ,left#(n) ,right#(left(n)) ,left#(n) ,right#(n) ,inc#(x)):1 3:S:if#(false(),true(),n,m,x,y) -> c_3(count#(n,y)) -->_1 count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,isEmpty#(n) ,isEmpty#(left(n)) ,left#(n) ,right#(n) ,left#(left(n)) ,left#(n) ,right#(left(n)) ,left#(n) ,right#(n) ,inc#(x)):1 4:S:inc#(s(x)) -> c_6(inc#(x)) -->_1 inc#(s(x)) -> c_6(inc#(x)):4 5:S:nrOfNodes#(n) -> c_11(count#(n,0())) -->_1 count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,isEmpty#(n) ,isEmpty#(left(n)) ,left#(n) ,right#(n) ,left#(left(n)) ,left#(n) ,right#(left(n)) ,left#(n) ,right#(n) ,inc#(x)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,inc#(x)) * Step 6: RemoveHeads MAYBE + Considered Problem: - Strict DPs: count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,inc#(x)) if#(false(),false(),n,m,x,y) -> c_2(count#(m,x)) if#(false(),true(),n,m,x,y) -> c_3(count#(n,y)) inc#(s(x)) -> c_6(inc#(x)) nrOfNodes#(n) -> c_11(count#(n,0())) - Weak TRS: inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(empty()) -> true() isEmpty(node(l,r)) -> false() left(empty()) -> empty() left(node(l,r)) -> l right(empty()) -> empty() right(node(l,r)) -> r - Signature: {count/2,if/6,inc/1,isEmpty/1,left/1,nrOfNodes/1,right/1,count#/2,if#/6,inc#/1,isEmpty#/1,left#/1 ,nrOfNodes#/1,right#/1} / {0/0,empty/0,false/0,node/2,s/1,true/0,c_1/2,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0 ,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {count#,if#,inc#,isEmpty#,left#,nrOfNodes# ,right#} and constructors {0,empty,false,node,s,true} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,inc#(x)) -->_2 inc#(s(x)) -> c_6(inc#(x)):4 -->_1 if#(false(),true(),n,m,x,y) -> c_3(count#(n,y)):3 -->_1 if#(false(),false(),n,m,x,y) -> c_2(count#(m,x)):2 2:S:if#(false(),false(),n,m,x,y) -> c_2(count#(m,x)) -->_1 count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,inc#(x)):1 3:S:if#(false(),true(),n,m,x,y) -> c_3(count#(n,y)) -->_1 count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,inc#(x)):1 4:S:inc#(s(x)) -> c_6(inc#(x)) -->_1 inc#(s(x)) -> c_6(inc#(x)):4 5:S:nrOfNodes#(n) -> c_11(count#(n,0())) -->_1 count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,inc#(x)):1 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(5,nrOfNodes#(n) -> c_11(count#(n,0())))] * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: count#(n,x) -> c_1(if#(isEmpty(n) ,isEmpty(left(n)) ,right(n) ,node(left(left(n)),node(right(left(n)),right(n))) ,x ,inc(x)) ,inc#(x)) if#(false(),false(),n,m,x,y) -> c_2(count#(m,x)) if#(false(),true(),n,m,x,y) -> c_3(count#(n,y)) inc#(s(x)) -> c_6(inc#(x)) - Weak TRS: inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(empty()) -> true() isEmpty(node(l,r)) -> false() left(empty()) -> empty() left(node(l,r)) -> l right(empty()) -> empty() right(node(l,r)) -> r - Signature: {count/2,if/6,inc/1,isEmpty/1,left/1,nrOfNodes/1,right/1,count#/2,if#/6,inc#/1,isEmpty#/1,left#/1 ,nrOfNodes#/1,right#/1} / {0/0,empty/0,false/0,node/2,s/1,true/0,c_1/2,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0 ,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {count#,if#,inc#,isEmpty#,left#,nrOfNodes# ,right#} and constructors {0,empty,false,node,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE