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