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