MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: addList(xs,ys) -> addLists(xs,ys,nil()) addLists(xs,ys,zs) -> if(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) append(cons(y,ys),x) -> cons(y,append(ys,x)) append(nil(),x) -> cons(x,nil()) head(cons(x,xs)) -> x if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs) if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2) if(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError() if(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError() if(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> zs inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(cons(x,xs)) -> false() isEmpty(nil()) -> true() isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {addList/2,addLists/3,append/2,head/1,if/9,inc/1,isEmpty/1,isZero/1,p/1,tail/1} / {0/0,cons/2 ,differentLengthError/0,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {addList,addLists,append,head,if,inc,isEmpty,isZero,p ,tail} and constructors {0,cons,differentLengthError,false,nil,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs addList#(xs,ys) -> c_1(addLists#(xs,ys,nil())) addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,isEmpty#(xs) ,isEmpty#(ys) ,isZero#(head(xs)) ,head#(xs) ,tail#(xs) ,tail#(ys) ,p#(head(xs)) ,head#(xs) ,tail#(xs) ,inc#(head(ys)) ,head#(ys) ,tail#(ys) ,append#(zs,head(ys)) ,head#(ys)) append#(cons(y,ys),x) -> c_3(append#(ys,x)) append#(nil(),x) -> c_4() head#(cons(x,xs)) -> c_5() if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> c_6(addLists#(xs2,ys2,zs)) if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> c_7(addLists#(xs,ys,zs2)) if#(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_8() if#(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> c_9() if#(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_10() inc#(0()) -> c_11() inc#(s(x)) -> c_12(inc#(x)) isEmpty#(cons(x,xs)) -> c_13() isEmpty#(nil()) -> c_14() isZero#(0()) -> c_15() isZero#(s(x)) -> c_16() p#(0()) -> c_17() p#(s(0())) -> c_18() p#(s(s(x))) -> c_19(p#(s(x))) tail#(cons(x,xs)) -> c_20() tail#(nil()) -> c_21() Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: addList#(xs,ys) -> c_1(addLists#(xs,ys,nil())) addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,isEmpty#(xs) ,isEmpty#(ys) ,isZero#(head(xs)) ,head#(xs) ,tail#(xs) ,tail#(ys) ,p#(head(xs)) ,head#(xs) ,tail#(xs) ,inc#(head(ys)) ,head#(ys) ,tail#(ys) ,append#(zs,head(ys)) ,head#(ys)) append#(cons(y,ys),x) -> c_3(append#(ys,x)) append#(nil(),x) -> c_4() head#(cons(x,xs)) -> c_5() if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> c_6(addLists#(xs2,ys2,zs)) if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> c_7(addLists#(xs,ys,zs2)) if#(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_8() if#(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> c_9() if#(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_10() inc#(0()) -> c_11() inc#(s(x)) -> c_12(inc#(x)) isEmpty#(cons(x,xs)) -> c_13() isEmpty#(nil()) -> c_14() isZero#(0()) -> c_15() isZero#(s(x)) -> c_16() p#(0()) -> c_17() p#(s(0())) -> c_18() p#(s(s(x))) -> c_19(p#(s(x))) tail#(cons(x,xs)) -> c_20() tail#(nil()) -> c_21() - Weak TRS: addList(xs,ys) -> addLists(xs,ys,nil()) addLists(xs,ys,zs) -> if(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) append(cons(y,ys),x) -> cons(y,append(ys,x)) append(nil(),x) -> cons(x,nil()) head(cons(x,xs)) -> x if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs) if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2) if(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError() if(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError() if(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> zs inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(cons(x,xs)) -> false() isEmpty(nil()) -> true() isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {addList/2,addLists/3,append/2,head/1,if/9,inc/1,isEmpty/1,isZero/1,p/1,tail/1,addList#/2,addLists#/3 ,append#/2,head#/1,if#/9,inc#/1,isEmpty#/1,isZero#/1,p#/1,tail#/1} / {0/0,cons/2,differentLengthError/0 ,false/0,nil/0,s/1,true/0,c_1/1,c_2/15,c_3/1,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0 ,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {addList#,addLists#,append#,head#,if#,inc#,isEmpty# ,isZero#,p#,tail#} and constructors {0,cons,differentLengthError,false,nil,s,true} + 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()) head(cons(x,xs)) -> x inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(cons(x,xs)) -> false() isEmpty(nil()) -> true() isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() addList#(xs,ys) -> c_1(addLists#(xs,ys,nil())) addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,isEmpty#(xs) ,isEmpty#(ys) ,isZero#(head(xs)) ,head#(xs) ,tail#(xs) ,tail#(ys) ,p#(head(xs)) ,head#(xs) ,tail#(xs) ,inc#(head(ys)) ,head#(ys) ,tail#(ys) ,append#(zs,head(ys)) ,head#(ys)) append#(cons(y,ys),x) -> c_3(append#(ys,x)) append#(nil(),x) -> c_4() head#(cons(x,xs)) -> c_5() if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> c_6(addLists#(xs2,ys2,zs)) if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> c_7(addLists#(xs,ys,zs2)) if#(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_8() if#(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> c_9() if#(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_10() inc#(0()) -> c_11() inc#(s(x)) -> c_12(inc#(x)) isEmpty#(cons(x,xs)) -> c_13() isEmpty#(nil()) -> c_14() isZero#(0()) -> c_15() isZero#(s(x)) -> c_16() p#(0()) -> c_17() p#(s(0())) -> c_18() p#(s(s(x))) -> c_19(p#(s(x))) tail#(cons(x,xs)) -> c_20() tail#(nil()) -> c_21() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: addList#(xs,ys) -> c_1(addLists#(xs,ys,nil())) addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,isEmpty#(xs) ,isEmpty#(ys) ,isZero#(head(xs)) ,head#(xs) ,tail#(xs) ,tail#(ys) ,p#(head(xs)) ,head#(xs) ,tail#(xs) ,inc#(head(ys)) ,head#(ys) ,tail#(ys) ,append#(zs,head(ys)) ,head#(ys)) append#(cons(y,ys),x) -> c_3(append#(ys,x)) append#(nil(),x) -> c_4() head#(cons(x,xs)) -> c_5() if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> c_6(addLists#(xs2,ys2,zs)) if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> c_7(addLists#(xs,ys,zs2)) if#(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_8() if#(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> c_9() if#(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_10() inc#(0()) -> c_11() inc#(s(x)) -> c_12(inc#(x)) isEmpty#(cons(x,xs)) -> c_13() isEmpty#(nil()) -> c_14() isZero#(0()) -> c_15() isZero#(s(x)) -> c_16() p#(0()) -> c_17() p#(s(0())) -> c_18() p#(s(s(x))) -> c_19(p#(s(x))) tail#(cons(x,xs)) -> c_20() tail#(nil()) -> c_21() - Weak TRS: append(cons(y,ys),x) -> cons(y,append(ys,x)) append(nil(),x) -> cons(x,nil()) head(cons(x,xs)) -> x inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(cons(x,xs)) -> false() isEmpty(nil()) -> true() isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {addList/2,addLists/3,append/2,head/1,if/9,inc/1,isEmpty/1,isZero/1,p/1,tail/1,addList#/2,addLists#/3 ,append#/2,head#/1,if#/9,inc#/1,isEmpty#/1,isZero#/1,p#/1,tail#/1} / {0/0,cons/2,differentLengthError/0 ,false/0,nil/0,s/1,true/0,c_1/1,c_2/15,c_3/1,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0 ,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {addList#,addLists#,append#,head#,if#,inc#,isEmpty# ,isZero#,p#,tail#} and constructors {0,cons,differentLengthError,false,nil,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {4,5,8,9,10,11,13,14,15,16,17,18,20,21} by application of Pre({4,5,8,9,10,11,13,14,15,16,17,18,20,21}) = {2,3,12,19}. Here rules are labelled as follows: 1: addList#(xs,ys) -> c_1(addLists#(xs,ys,nil())) 2: addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,isEmpty#(xs) ,isEmpty#(ys) ,isZero#(head(xs)) ,head#(xs) ,tail#(xs) ,tail#(ys) ,p#(head(xs)) ,head#(xs) ,tail#(xs) ,inc#(head(ys)) ,head#(ys) ,tail#(ys) ,append#(zs,head(ys)) ,head#(ys)) 3: append#(cons(y,ys),x) -> c_3(append#(ys,x)) 4: append#(nil(),x) -> c_4() 5: head#(cons(x,xs)) -> c_5() 6: if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> c_6(addLists#(xs2,ys2,zs)) 7: if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> c_7(addLists#(xs,ys,zs2)) 8: if#(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_8() 9: if#(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> c_9() 10: if#(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_10() 11: inc#(0()) -> c_11() 12: inc#(s(x)) -> c_12(inc#(x)) 13: isEmpty#(cons(x,xs)) -> c_13() 14: isEmpty#(nil()) -> c_14() 15: isZero#(0()) -> c_15() 16: isZero#(s(x)) -> c_16() 17: p#(0()) -> c_17() 18: p#(s(0())) -> c_18() 19: p#(s(s(x))) -> c_19(p#(s(x))) 20: tail#(cons(x,xs)) -> c_20() 21: tail#(nil()) -> c_21() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: addList#(xs,ys) -> c_1(addLists#(xs,ys,nil())) addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,isEmpty#(xs) ,isEmpty#(ys) ,isZero#(head(xs)) ,head#(xs) ,tail#(xs) ,tail#(ys) ,p#(head(xs)) ,head#(xs) ,tail#(xs) ,inc#(head(ys)) ,head#(ys) ,tail#(ys) ,append#(zs,head(ys)) ,head#(ys)) append#(cons(y,ys),x) -> c_3(append#(ys,x)) if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> c_6(addLists#(xs2,ys2,zs)) if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> c_7(addLists#(xs,ys,zs2)) inc#(s(x)) -> c_12(inc#(x)) p#(s(s(x))) -> c_19(p#(s(x))) - Weak DPs: append#(nil(),x) -> c_4() head#(cons(x,xs)) -> c_5() if#(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_8() if#(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> c_9() if#(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_10() inc#(0()) -> c_11() isEmpty#(cons(x,xs)) -> c_13() isEmpty#(nil()) -> c_14() isZero#(0()) -> c_15() isZero#(s(x)) -> c_16() p#(0()) -> c_17() p#(s(0())) -> c_18() tail#(cons(x,xs)) -> c_20() tail#(nil()) -> c_21() - Weak TRS: append(cons(y,ys),x) -> cons(y,append(ys,x)) append(nil(),x) -> cons(x,nil()) head(cons(x,xs)) -> x inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(cons(x,xs)) -> false() isEmpty(nil()) -> true() isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {addList/2,addLists/3,append/2,head/1,if/9,inc/1,isEmpty/1,isZero/1,p/1,tail/1,addList#/2,addLists#/3 ,append#/2,head#/1,if#/9,inc#/1,isEmpty#/1,isZero#/1,p#/1,tail#/1} / {0/0,cons/2,differentLengthError/0 ,false/0,nil/0,s/1,true/0,c_1/1,c_2/15,c_3/1,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0 ,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {addList#,addLists#,append#,head#,if#,inc#,isEmpty# ,isZero#,p#,tail#} and constructors {0,cons,differentLengthError,false,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:addList#(xs,ys) -> c_1(addLists#(xs,ys,nil())) -->_1 addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,isEmpty#(xs) ,isEmpty#(ys) ,isZero#(head(xs)) ,head#(xs) ,tail#(xs) ,tail#(ys) ,p#(head(xs)) ,head#(xs) ,tail#(xs) ,inc#(head(ys)) ,head#(ys) ,tail#(ys) ,append#(zs,head(ys)) ,head#(ys)):2 2:S:addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,isEmpty#(xs) ,isEmpty#(ys) ,isZero#(head(xs)) ,head#(xs) ,tail#(xs) ,tail#(ys) ,p#(head(xs)) ,head#(xs) ,tail#(xs) ,inc#(head(ys)) ,head#(ys) ,tail#(ys) ,append#(zs,head(ys)) ,head#(ys)) -->_8 p#(s(s(x))) -> c_19(p#(s(x))):7 -->_11 inc#(s(x)) -> c_12(inc#(x)):6 -->_1 if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> c_7(addLists#(xs,ys,zs2)):5 -->_1 if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> c_6(addLists#(xs2,ys2,zs)):4 -->_14 append#(cons(y,ys),x) -> c_3(append#(ys,x)):3 -->_13 tail#(nil()) -> c_21():21 -->_10 tail#(nil()) -> c_21():21 -->_7 tail#(nil()) -> c_21():21 -->_6 tail#(nil()) -> c_21():21 -->_13 tail#(cons(x,xs)) -> c_20():20 -->_10 tail#(cons(x,xs)) -> c_20():20 -->_7 tail#(cons(x,xs)) -> c_20():20 -->_6 tail#(cons(x,xs)) -> c_20():20 -->_8 p#(s(0())) -> c_18():19 -->_8 p#(0()) -> c_17():18 -->_4 isZero#(s(x)) -> c_16():17 -->_4 isZero#(0()) -> c_15():16 -->_3 isEmpty#(nil()) -> c_14():15 -->_2 isEmpty#(nil()) -> c_14():15 -->_3 isEmpty#(cons(x,xs)) -> c_13():14 -->_2 isEmpty#(cons(x,xs)) -> c_13():14 -->_11 inc#(0()) -> c_11():13 -->_1 if#(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_10():12 -->_1 if#(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> c_9():11 -->_1 if#(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_8():10 -->_15 head#(cons(x,xs)) -> c_5():9 -->_12 head#(cons(x,xs)) -> c_5():9 -->_9 head#(cons(x,xs)) -> c_5():9 -->_5 head#(cons(x,xs)) -> c_5():9 -->_14 append#(nil(),x) -> c_4():8 3:S:append#(cons(y,ys),x) -> c_3(append#(ys,x)) -->_1 append#(nil(),x) -> c_4():8 -->_1 append#(cons(y,ys),x) -> c_3(append#(ys,x)):3 4:S:if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> c_6(addLists#(xs2,ys2,zs)) -->_1 addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,isEmpty#(xs) ,isEmpty#(ys) ,isZero#(head(xs)) ,head#(xs) ,tail#(xs) ,tail#(ys) ,p#(head(xs)) ,head#(xs) ,tail#(xs) ,inc#(head(ys)) ,head#(ys) ,tail#(ys) ,append#(zs,head(ys)) ,head#(ys)):2 5:S:if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> c_7(addLists#(xs,ys,zs2)) -->_1 addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,isEmpty#(xs) ,isEmpty#(ys) ,isZero#(head(xs)) ,head#(xs) ,tail#(xs) ,tail#(ys) ,p#(head(xs)) ,head#(xs) ,tail#(xs) ,inc#(head(ys)) ,head#(ys) ,tail#(ys) ,append#(zs,head(ys)) ,head#(ys)):2 6:S:inc#(s(x)) -> c_12(inc#(x)) -->_1 inc#(0()) -> c_11():13 -->_1 inc#(s(x)) -> c_12(inc#(x)):6 7:S:p#(s(s(x))) -> c_19(p#(s(x))) -->_1 p#(s(0())) -> c_18():19 -->_1 p#(s(s(x))) -> c_19(p#(s(x))):7 8:W:append#(nil(),x) -> c_4() 9:W:head#(cons(x,xs)) -> c_5() 10:W:if#(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_8() 11:W:if#(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> c_9() 12:W:if#(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_10() 13:W:inc#(0()) -> c_11() 14:W:isEmpty#(cons(x,xs)) -> c_13() 15:W:isEmpty#(nil()) -> c_14() 16:W:isZero#(0()) -> c_15() 17:W:isZero#(s(x)) -> c_16() 18:W:p#(0()) -> c_17() 19:W:p#(s(0())) -> c_18() 20:W:tail#(cons(x,xs)) -> c_20() 21:W:tail#(nil()) -> c_21() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 9: head#(cons(x,xs)) -> c_5() 10: if#(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_8() 11: if#(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> c_9() 12: if#(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> c_10() 14: isEmpty#(cons(x,xs)) -> c_13() 15: isEmpty#(nil()) -> c_14() 16: isZero#(0()) -> c_15() 17: isZero#(s(x)) -> c_16() 18: p#(0()) -> c_17() 20: tail#(cons(x,xs)) -> c_20() 21: tail#(nil()) -> c_21() 8: append#(nil(),x) -> c_4() 13: inc#(0()) -> c_11() 19: p#(s(0())) -> c_18() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: addList#(xs,ys) -> c_1(addLists#(xs,ys,nil())) addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,isEmpty#(xs) ,isEmpty#(ys) ,isZero#(head(xs)) ,head#(xs) ,tail#(xs) ,tail#(ys) ,p#(head(xs)) ,head#(xs) ,tail#(xs) ,inc#(head(ys)) ,head#(ys) ,tail#(ys) ,append#(zs,head(ys)) ,head#(ys)) append#(cons(y,ys),x) -> c_3(append#(ys,x)) if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> c_6(addLists#(xs2,ys2,zs)) if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> c_7(addLists#(xs,ys,zs2)) inc#(s(x)) -> c_12(inc#(x)) p#(s(s(x))) -> c_19(p#(s(x))) - Weak TRS: append(cons(y,ys),x) -> cons(y,append(ys,x)) append(nil(),x) -> cons(x,nil()) head(cons(x,xs)) -> x inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(cons(x,xs)) -> false() isEmpty(nil()) -> true() isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {addList/2,addLists/3,append/2,head/1,if/9,inc/1,isEmpty/1,isZero/1,p/1,tail/1,addList#/2,addLists#/3 ,append#/2,head#/1,if#/9,inc#/1,isEmpty#/1,isZero#/1,p#/1,tail#/1} / {0/0,cons/2,differentLengthError/0 ,false/0,nil/0,s/1,true/0,c_1/1,c_2/15,c_3/1,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0 ,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {addList#,addLists#,append#,head#,if#,inc#,isEmpty# ,isZero#,p#,tail#} and constructors {0,cons,differentLengthError,false,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:addList#(xs,ys) -> c_1(addLists#(xs,ys,nil())) -->_1 addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,isEmpty#(xs) ,isEmpty#(ys) ,isZero#(head(xs)) ,head#(xs) ,tail#(xs) ,tail#(ys) ,p#(head(xs)) ,head#(xs) ,tail#(xs) ,inc#(head(ys)) ,head#(ys) ,tail#(ys) ,append#(zs,head(ys)) ,head#(ys)):2 2:S:addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,isEmpty#(xs) ,isEmpty#(ys) ,isZero#(head(xs)) ,head#(xs) ,tail#(xs) ,tail#(ys) ,p#(head(xs)) ,head#(xs) ,tail#(xs) ,inc#(head(ys)) ,head#(ys) ,tail#(ys) ,append#(zs,head(ys)) ,head#(ys)) -->_8 p#(s(s(x))) -> c_19(p#(s(x))):7 -->_11 inc#(s(x)) -> c_12(inc#(x)):6 -->_1 if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> c_7(addLists#(xs,ys,zs2)):5 -->_1 if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> c_6(addLists#(xs2,ys2,zs)):4 -->_14 append#(cons(y,ys),x) -> c_3(append#(ys,x)):3 3:S:append#(cons(y,ys),x) -> c_3(append#(ys,x)) -->_1 append#(cons(y,ys),x) -> c_3(append#(ys,x)):3 4:S:if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> c_6(addLists#(xs2,ys2,zs)) -->_1 addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,isEmpty#(xs) ,isEmpty#(ys) ,isZero#(head(xs)) ,head#(xs) ,tail#(xs) ,tail#(ys) ,p#(head(xs)) ,head#(xs) ,tail#(xs) ,inc#(head(ys)) ,head#(ys) ,tail#(ys) ,append#(zs,head(ys)) ,head#(ys)):2 5:S:if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> c_7(addLists#(xs,ys,zs2)) -->_1 addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,isEmpty#(xs) ,isEmpty#(ys) ,isZero#(head(xs)) ,head#(xs) ,tail#(xs) ,tail#(ys) ,p#(head(xs)) ,head#(xs) ,tail#(xs) ,inc#(head(ys)) ,head#(ys) ,tail#(ys) ,append#(zs,head(ys)) ,head#(ys)):2 6:S:inc#(s(x)) -> c_12(inc#(x)) -->_1 inc#(s(x)) -> c_12(inc#(x)):6 7:S:p#(s(s(x))) -> c_19(p#(s(x))) -->_1 p#(s(s(x))) -> c_19(p#(s(x))):7 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,p#(head(xs)) ,inc#(head(ys)) ,append#(zs,head(ys))) * Step 6: RemoveHeads MAYBE + Considered Problem: - Strict DPs: addList#(xs,ys) -> c_1(addLists#(xs,ys,nil())) addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,p#(head(xs)) ,inc#(head(ys)) ,append#(zs,head(ys))) append#(cons(y,ys),x) -> c_3(append#(ys,x)) if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> c_6(addLists#(xs2,ys2,zs)) if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> c_7(addLists#(xs,ys,zs2)) inc#(s(x)) -> c_12(inc#(x)) p#(s(s(x))) -> c_19(p#(s(x))) - Weak TRS: append(cons(y,ys),x) -> cons(y,append(ys,x)) append(nil(),x) -> cons(x,nil()) head(cons(x,xs)) -> x inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(cons(x,xs)) -> false() isEmpty(nil()) -> true() isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {addList/2,addLists/3,append/2,head/1,if/9,inc/1,isEmpty/1,isZero/1,p/1,tail/1,addList#/2,addLists#/3 ,append#/2,head#/1,if#/9,inc#/1,isEmpty#/1,isZero#/1,p#/1,tail#/1} / {0/0,cons/2,differentLengthError/0 ,false/0,nil/0,s/1,true/0,c_1/1,c_2/4,c_3/1,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0 ,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {addList#,addLists#,append#,head#,if#,inc#,isEmpty# ,isZero#,p#,tail#} and constructors {0,cons,differentLengthError,false,nil,s,true} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:addList#(xs,ys) -> c_1(addLists#(xs,ys,nil())) -->_1 addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,p#(head(xs)) ,inc#(head(ys)) ,append#(zs,head(ys))):2 2:S:addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,p#(head(xs)) ,inc#(head(ys)) ,append#(zs,head(ys))) -->_2 p#(s(s(x))) -> c_19(p#(s(x))):7 -->_3 inc#(s(x)) -> c_12(inc#(x)):6 -->_1 if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> c_7(addLists#(xs,ys,zs2)):5 -->_1 if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> c_6(addLists#(xs2,ys2,zs)):4 -->_4 append#(cons(y,ys),x) -> c_3(append#(ys,x)):3 3:S:append#(cons(y,ys),x) -> c_3(append#(ys,x)) -->_1 append#(cons(y,ys),x) -> c_3(append#(ys,x)):3 4:S:if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> c_6(addLists#(xs2,ys2,zs)) -->_1 addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,p#(head(xs)) ,inc#(head(ys)) ,append#(zs,head(ys))):2 5:S:if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> c_7(addLists#(xs,ys,zs2)) -->_1 addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,p#(head(xs)) ,inc#(head(ys)) ,append#(zs,head(ys))):2 6:S:inc#(s(x)) -> c_12(inc#(x)) -->_1 inc#(s(x)) -> c_12(inc#(x)):6 7:S:p#(s(s(x))) -> c_19(p#(s(x))) -->_1 p#(s(s(x))) -> c_19(p#(s(x))):7 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). [(1,addList#(xs,ys) -> c_1(addLists#(xs,ys,nil())))] * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: addLists#(xs,ys,zs) -> c_2(if#(isEmpty(xs) ,isEmpty(ys) ,isZero(head(xs)) ,tail(xs) ,tail(ys) ,cons(p(head(xs)),tail(xs)) ,cons(inc(head(ys)),tail(ys)) ,zs ,append(zs,head(ys))) ,p#(head(xs)) ,inc#(head(ys)) ,append#(zs,head(ys))) append#(cons(y,ys),x) -> c_3(append#(ys,x)) if#(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> c_6(addLists#(xs2,ys2,zs)) if#(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> c_7(addLists#(xs,ys,zs2)) inc#(s(x)) -> c_12(inc#(x)) p#(s(s(x))) -> c_19(p#(s(x))) - Weak TRS: append(cons(y,ys),x) -> cons(y,append(ys,x)) append(nil(),x) -> cons(x,nil()) head(cons(x,xs)) -> x inc(0()) -> s(0()) inc(s(x)) -> s(inc(x)) isEmpty(cons(x,xs)) -> false() isEmpty(nil()) -> true() isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {addList/2,addLists/3,append/2,head/1,if/9,inc/1,isEmpty/1,isZero/1,p/1,tail/1,addList#/2,addLists#/3 ,append#/2,head#/1,if#/9,inc#/1,isEmpty#/1,isZero#/1,p#/1,tail#/1} / {0/0,cons/2,differentLengthError/0 ,false/0,nil/0,s/1,true/0,c_1/1,c_2/4,c_3/1,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0 ,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {addList#,addLists#,append#,head#,if#,inc#,isEmpty# ,isZero#,p#,tail#} and constructors {0,cons,differentLengthError,false,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE