MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: activate(X) -> X activate(n__dbl(X)) -> dbl(activate(X)) activate(n__dbls(X)) -> dbls(activate(X)) activate(n__from(X)) -> from(X) activate(n__indx(X1,X2)) -> indx(activate(X1),X2) activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) dbl(X) -> n__dbl(X) dbl(0()) -> 0() dbl(s(X)) -> s(n__s(n__dbl(activate(X)))) dbls(X) -> n__dbls(X) dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y))) dbls(nil()) -> nil() from(X) -> cons(activate(X),n__from(n__s(activate(X)))) from(X) -> n__from(X) indx(X1,X2) -> n__indx(X1,X2) indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) indx(nil(),X) -> nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) sel(0(),cons(X,Y)) -> activate(X) sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z)) - Signature: {activate/1,dbl/1,dbls/1,from/1,indx/2,s/1,sel/2} / {0/0,cons/2,n__dbl/1,n__dbls/1,n__from/1,n__indx/2 ,n__s/1,n__sel/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate,dbl,dbls,from,indx,s,sel} and constructors {0 ,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. dbl(s(X)) -> s(n__s(n__dbl(activate(X)))) sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z)) All above mentioned rules can be savely removed. * Step 2: DependencyPairs MAYBE + Considered Problem: - Strict TRS: activate(X) -> X activate(n__dbl(X)) -> dbl(activate(X)) activate(n__dbls(X)) -> dbls(activate(X)) activate(n__from(X)) -> from(X) activate(n__indx(X1,X2)) -> indx(activate(X1),X2) activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) dbl(X) -> n__dbl(X) dbl(0()) -> 0() dbls(X) -> n__dbls(X) dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y))) dbls(nil()) -> nil() from(X) -> cons(activate(X),n__from(n__s(activate(X)))) from(X) -> n__from(X) indx(X1,X2) -> n__indx(X1,X2) indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) indx(nil(),X) -> nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) sel(0(),cons(X,Y)) -> activate(X) - Signature: {activate/1,dbl/1,dbls/1,from/1,indx/2,s/1,sel/2} / {0/0,cons/2,n__dbl/1,n__dbls/1,n__from/1,n__indx/2 ,n__s/1,n__sel/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate,dbl,dbls,from,indx,s,sel} and constructors {0 ,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs activate#(X) -> c_1() activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)) activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)) activate#(n__from(X)) -> c_4(from#(X)) activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)) activate#(n__s(X)) -> c_6(s#(X)) activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) dbl#(X) -> c_8() dbl#(0()) -> c_9() dbls#(X) -> c_10() dbls#(cons(X,Y)) -> c_11(activate#(X),activate#(Y)) dbls#(nil()) -> c_12() from#(X) -> c_13(activate#(X),activate#(X)) from#(X) -> c_14() indx#(X1,X2) -> c_15() indx#(cons(X,Y),Z) -> c_16(activate#(X),activate#(Z),activate#(Y),activate#(Z)) indx#(nil(),X) -> c_17() s#(X) -> c_18() sel#(X1,X2) -> c_19() sel#(0(),cons(X,Y)) -> c_20(activate#(X)) Weak DPs and mark the set of starting terms. * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(X) -> c_1() activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)) activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)) activate#(n__from(X)) -> c_4(from#(X)) activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)) activate#(n__s(X)) -> c_6(s#(X)) activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) dbl#(X) -> c_8() dbl#(0()) -> c_9() dbls#(X) -> c_10() dbls#(cons(X,Y)) -> c_11(activate#(X),activate#(Y)) dbls#(nil()) -> c_12() from#(X) -> c_13(activate#(X),activate#(X)) from#(X) -> c_14() indx#(X1,X2) -> c_15() indx#(cons(X,Y),Z) -> c_16(activate#(X),activate#(Z),activate#(Y),activate#(Z)) indx#(nil(),X) -> c_17() s#(X) -> c_18() sel#(X1,X2) -> c_19() sel#(0(),cons(X,Y)) -> c_20(activate#(X)) - Weak TRS: activate(X) -> X activate(n__dbl(X)) -> dbl(activate(X)) activate(n__dbls(X)) -> dbls(activate(X)) activate(n__from(X)) -> from(X) activate(n__indx(X1,X2)) -> indx(activate(X1),X2) activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) dbl(X) -> n__dbl(X) dbl(0()) -> 0() dbls(X) -> n__dbls(X) dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y))) dbls(nil()) -> nil() from(X) -> cons(activate(X),n__from(n__s(activate(X)))) from(X) -> n__from(X) indx(X1,X2) -> n__indx(X1,X2) indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) indx(nil(),X) -> nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) sel(0(),cons(X,Y)) -> activate(X) - Signature: {activate/1,dbl/1,dbls/1,from/1,indx/2,s/1,sel/2,activate#/1,dbl#/1,dbls#/1,from#/1,indx#/2,s#/1 ,sel#/2} / {0/0,cons/2,n__dbl/1,n__dbls/1,n__from/1,n__indx/2,n__s/1,n__sel/2,nil/0,c_1/0,c_2/2,c_3/2,c_4/1 ,c_5/2,c_6/1,c_7/3,c_8/0,c_9/0,c_10/0,c_11/2,c_12/0,c_13/2,c_14/0,c_15/0,c_16/4,c_17/0,c_18/0,c_19/0,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,dbl#,dbls#,from#,indx#,s# ,sel#} and constructors {0,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,8,9,10,12,14,15,17,18,19} by application of Pre({1,8,9,10,12,14,15,17,18,19}) = {2,3,4,5,6,7,11,13,16,20}. Here rules are labelled as follows: 1: activate#(X) -> c_1() 2: activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)) 3: activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)) 4: activate#(n__from(X)) -> c_4(from#(X)) 5: activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)) 6: activate#(n__s(X)) -> c_6(s#(X)) 7: activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 8: dbl#(X) -> c_8() 9: dbl#(0()) -> c_9() 10: dbls#(X) -> c_10() 11: dbls#(cons(X,Y)) -> c_11(activate#(X),activate#(Y)) 12: dbls#(nil()) -> c_12() 13: from#(X) -> c_13(activate#(X),activate#(X)) 14: from#(X) -> c_14() 15: indx#(X1,X2) -> c_15() 16: indx#(cons(X,Y),Z) -> c_16(activate#(X),activate#(Z),activate#(Y),activate#(Z)) 17: indx#(nil(),X) -> c_17() 18: s#(X) -> c_18() 19: sel#(X1,X2) -> c_19() 20: sel#(0(),cons(X,Y)) -> c_20(activate#(X)) * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)) activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)) activate#(n__from(X)) -> c_4(from#(X)) activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)) activate#(n__s(X)) -> c_6(s#(X)) activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) dbls#(cons(X,Y)) -> c_11(activate#(X),activate#(Y)) from#(X) -> c_13(activate#(X),activate#(X)) indx#(cons(X,Y),Z) -> c_16(activate#(X),activate#(Z),activate#(Y),activate#(Z)) sel#(0(),cons(X,Y)) -> c_20(activate#(X)) - Weak DPs: activate#(X) -> c_1() dbl#(X) -> c_8() dbl#(0()) -> c_9() dbls#(X) -> c_10() dbls#(nil()) -> c_12() from#(X) -> c_14() indx#(X1,X2) -> c_15() indx#(nil(),X) -> c_17() s#(X) -> c_18() sel#(X1,X2) -> c_19() - Weak TRS: activate(X) -> X activate(n__dbl(X)) -> dbl(activate(X)) activate(n__dbls(X)) -> dbls(activate(X)) activate(n__from(X)) -> from(X) activate(n__indx(X1,X2)) -> indx(activate(X1),X2) activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) dbl(X) -> n__dbl(X) dbl(0()) -> 0() dbls(X) -> n__dbls(X) dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y))) dbls(nil()) -> nil() from(X) -> cons(activate(X),n__from(n__s(activate(X)))) from(X) -> n__from(X) indx(X1,X2) -> n__indx(X1,X2) indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) indx(nil(),X) -> nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) sel(0(),cons(X,Y)) -> activate(X) - Signature: {activate/1,dbl/1,dbls/1,from/1,indx/2,s/1,sel/2,activate#/1,dbl#/1,dbls#/1,from#/1,indx#/2,s#/1 ,sel#/2} / {0/0,cons/2,n__dbl/1,n__dbls/1,n__from/1,n__indx/2,n__s/1,n__sel/2,nil/0,c_1/0,c_2/2,c_3/2,c_4/1 ,c_5/2,c_6/1,c_7/3,c_8/0,c_9/0,c_10/0,c_11/2,c_12/0,c_13/2,c_14/0,c_15/0,c_16/4,c_17/0,c_18/0,c_19/0,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,dbl#,dbls#,from#,indx#,s# ,sel#} and constructors {0,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {5} by application of Pre({5}) = {1,2,4,6,7,8,9,10}. Here rules are labelled as follows: 1: activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)) 2: activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)) 3: activate#(n__from(X)) -> c_4(from#(X)) 4: activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)) 5: activate#(n__s(X)) -> c_6(s#(X)) 6: activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 7: dbls#(cons(X,Y)) -> c_11(activate#(X),activate#(Y)) 8: from#(X) -> c_13(activate#(X),activate#(X)) 9: indx#(cons(X,Y),Z) -> c_16(activate#(X),activate#(Z),activate#(Y),activate#(Z)) 10: sel#(0(),cons(X,Y)) -> c_20(activate#(X)) 11: activate#(X) -> c_1() 12: dbl#(X) -> c_8() 13: dbl#(0()) -> c_9() 14: dbls#(X) -> c_10() 15: dbls#(nil()) -> c_12() 16: from#(X) -> c_14() 17: indx#(X1,X2) -> c_15() 18: indx#(nil(),X) -> c_17() 19: s#(X) -> c_18() 20: sel#(X1,X2) -> c_19() * Step 5: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)) activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)) activate#(n__from(X)) -> c_4(from#(X)) activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)) activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) dbls#(cons(X,Y)) -> c_11(activate#(X),activate#(Y)) from#(X) -> c_13(activate#(X),activate#(X)) indx#(cons(X,Y),Z) -> c_16(activate#(X),activate#(Z),activate#(Y),activate#(Z)) sel#(0(),cons(X,Y)) -> c_20(activate#(X)) - Weak DPs: activate#(X) -> c_1() activate#(n__s(X)) -> c_6(s#(X)) dbl#(X) -> c_8() dbl#(0()) -> c_9() dbls#(X) -> c_10() dbls#(nil()) -> c_12() from#(X) -> c_14() indx#(X1,X2) -> c_15() indx#(nil(),X) -> c_17() s#(X) -> c_18() sel#(X1,X2) -> c_19() - Weak TRS: activate(X) -> X activate(n__dbl(X)) -> dbl(activate(X)) activate(n__dbls(X)) -> dbls(activate(X)) activate(n__from(X)) -> from(X) activate(n__indx(X1,X2)) -> indx(activate(X1),X2) activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) dbl(X) -> n__dbl(X) dbl(0()) -> 0() dbls(X) -> n__dbls(X) dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y))) dbls(nil()) -> nil() from(X) -> cons(activate(X),n__from(n__s(activate(X)))) from(X) -> n__from(X) indx(X1,X2) -> n__indx(X1,X2) indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) indx(nil(),X) -> nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) sel(0(),cons(X,Y)) -> activate(X) - Signature: {activate/1,dbl/1,dbls/1,from/1,indx/2,s/1,sel/2,activate#/1,dbl#/1,dbls#/1,from#/1,indx#/2,s#/1 ,sel#/2} / {0/0,cons/2,n__dbl/1,n__dbls/1,n__from/1,n__indx/2,n__s/1,n__sel/2,nil/0,c_1/0,c_2/2,c_3/2,c_4/1 ,c_5/2,c_6/1,c_7/3,c_8/0,c_9/0,c_10/0,c_11/2,c_12/0,c_13/2,c_14/0,c_15/0,c_16/4,c_17/0,c_18/0,c_19/0,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,dbl#,dbls#,from#,indx#,s# ,sel#} and constructors {0,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)) -->_2 activate#(n__s(X)) -> c_6(s#(X)):11 -->_2 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_2 activate#(n__from(X)) -> c_4(from#(X)):3 -->_2 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_1 dbl#(0()) -> c_9():13 -->_1 dbl#(X) -> c_8():12 -->_2 activate#(X) -> c_1():10 -->_2 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 2:S:activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)) -->_2 activate#(n__s(X)) -> c_6(s#(X)):11 -->_1 dbls#(cons(X,Y)) -> c_11(activate#(X),activate#(Y)):6 -->_2 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_2 activate#(n__from(X)) -> c_4(from#(X)):3 -->_1 dbls#(nil()) -> c_12():15 -->_1 dbls#(X) -> c_10():14 -->_2 activate#(X) -> c_1():10 -->_2 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_2 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 3:S:activate#(n__from(X)) -> c_4(from#(X)) -->_1 from#(X) -> c_13(activate#(X),activate#(X)):7 -->_1 from#(X) -> c_14():16 4:S:activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)) -->_2 activate#(n__s(X)) -> c_6(s#(X)):11 -->_1 indx#(cons(X,Y),Z) -> c_16(activate#(X),activate#(Z),activate#(Y),activate#(Z)):8 -->_2 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 indx#(nil(),X) -> c_17():18 -->_1 indx#(X1,X2) -> c_15():17 -->_2 activate#(X) -> c_1():10 -->_2 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_2 activate#(n__from(X)) -> c_4(from#(X)):3 -->_2 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_2 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 5:S:activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__s(X)) -> c_6(s#(X)):11 -->_2 activate#(n__s(X)) -> c_6(s#(X)):11 -->_1 sel#(0(),cons(X,Y)) -> c_20(activate#(X)):9 -->_1 sel#(X1,X2) -> c_19():20 -->_3 activate#(X) -> c_1():10 -->_2 activate#(X) -> c_1():10 -->_3 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_2 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_3 activate#(n__from(X)) -> c_4(from#(X)):3 -->_2 activate#(n__from(X)) -> c_4(from#(X)):3 -->_3 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_2 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_3 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 -->_2 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 6:S:dbls#(cons(X,Y)) -> c_11(activate#(X),activate#(Y)) -->_2 activate#(n__s(X)) -> c_6(s#(X)):11 -->_1 activate#(n__s(X)) -> c_6(s#(X)):11 -->_2 activate#(X) -> c_1():10 -->_1 activate#(X) -> c_1():10 -->_2 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_1 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_2 activate#(n__from(X)) -> c_4(from#(X)):3 -->_1 activate#(n__from(X)) -> c_4(from#(X)):3 -->_2 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_1 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_2 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 -->_1 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 7:S:from#(X) -> c_13(activate#(X),activate#(X)) -->_2 activate#(n__s(X)) -> c_6(s#(X)):11 -->_1 activate#(n__s(X)) -> c_6(s#(X)):11 -->_2 activate#(X) -> c_1():10 -->_1 activate#(X) -> c_1():10 -->_2 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_1 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_2 activate#(n__from(X)) -> c_4(from#(X)):3 -->_1 activate#(n__from(X)) -> c_4(from#(X)):3 -->_2 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_1 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_2 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 -->_1 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 8:S:indx#(cons(X,Y),Z) -> c_16(activate#(X),activate#(Z),activate#(Y),activate#(Z)) -->_4 activate#(n__s(X)) -> c_6(s#(X)):11 -->_3 activate#(n__s(X)) -> c_6(s#(X)):11 -->_2 activate#(n__s(X)) -> c_6(s#(X)):11 -->_1 activate#(n__s(X)) -> c_6(s#(X)):11 -->_4 activate#(X) -> c_1():10 -->_3 activate#(X) -> c_1():10 -->_2 activate#(X) -> c_1():10 -->_1 activate#(X) -> c_1():10 -->_4 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_4 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_3 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_2 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_1 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_4 activate#(n__from(X)) -> c_4(from#(X)):3 -->_3 activate#(n__from(X)) -> c_4(from#(X)):3 -->_2 activate#(n__from(X)) -> c_4(from#(X)):3 -->_1 activate#(n__from(X)) -> c_4(from#(X)):3 -->_4 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_3 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_2 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_1 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_4 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 -->_3 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 -->_2 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 -->_1 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 9:S:sel#(0(),cons(X,Y)) -> c_20(activate#(X)) -->_1 activate#(n__s(X)) -> c_6(s#(X)):11 -->_1 activate#(X) -> c_1():10 -->_1 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_1 activate#(n__from(X)) -> c_4(from#(X)):3 -->_1 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_1 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 10:W:activate#(X) -> c_1() 11:W:activate#(n__s(X)) -> c_6(s#(X)) -->_1 s#(X) -> c_18():19 12:W:dbl#(X) -> c_8() 13:W:dbl#(0()) -> c_9() 14:W:dbls#(X) -> c_10() 15:W:dbls#(nil()) -> c_12() 16:W:from#(X) -> c_14() 17:W:indx#(X1,X2) -> c_15() 18:W:indx#(nil(),X) -> c_17() 19:W:s#(X) -> c_18() 20:W:sel#(X1,X2) -> c_19() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 12: dbl#(X) -> c_8() 13: dbl#(0()) -> c_9() 20: sel#(X1,X2) -> c_19() 17: indx#(X1,X2) -> c_15() 18: indx#(nil(),X) -> c_17() 16: from#(X) -> c_14() 14: dbls#(X) -> c_10() 15: dbls#(nil()) -> c_12() 10: activate#(X) -> c_1() 11: activate#(n__s(X)) -> c_6(s#(X)) 19: s#(X) -> c_18() * Step 6: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)) activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)) activate#(n__from(X)) -> c_4(from#(X)) activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)) activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) dbls#(cons(X,Y)) -> c_11(activate#(X),activate#(Y)) from#(X) -> c_13(activate#(X),activate#(X)) indx#(cons(X,Y),Z) -> c_16(activate#(X),activate#(Z),activate#(Y),activate#(Z)) sel#(0(),cons(X,Y)) -> c_20(activate#(X)) - Weak TRS: activate(X) -> X activate(n__dbl(X)) -> dbl(activate(X)) activate(n__dbls(X)) -> dbls(activate(X)) activate(n__from(X)) -> from(X) activate(n__indx(X1,X2)) -> indx(activate(X1),X2) activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) dbl(X) -> n__dbl(X) dbl(0()) -> 0() dbls(X) -> n__dbls(X) dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y))) dbls(nil()) -> nil() from(X) -> cons(activate(X),n__from(n__s(activate(X)))) from(X) -> n__from(X) indx(X1,X2) -> n__indx(X1,X2) indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) indx(nil(),X) -> nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) sel(0(),cons(X,Y)) -> activate(X) - Signature: {activate/1,dbl/1,dbls/1,from/1,indx/2,s/1,sel/2,activate#/1,dbl#/1,dbls#/1,from#/1,indx#/2,s#/1 ,sel#/2} / {0/0,cons/2,n__dbl/1,n__dbls/1,n__from/1,n__indx/2,n__s/1,n__sel/2,nil/0,c_1/0,c_2/2,c_3/2,c_4/1 ,c_5/2,c_6/1,c_7/3,c_8/0,c_9/0,c_10/0,c_11/2,c_12/0,c_13/2,c_14/0,c_15/0,c_16/4,c_17/0,c_18/0,c_19/0,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,dbl#,dbls#,from#,indx#,s# ,sel#} and constructors {0,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)) -->_2 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_2 activate#(n__from(X)) -> c_4(from#(X)):3 -->_2 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_2 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 2:S:activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)) -->_1 dbls#(cons(X,Y)) -> c_11(activate#(X),activate#(Y)):6 -->_2 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_2 activate#(n__from(X)) -> c_4(from#(X)):3 -->_2 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_2 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 3:S:activate#(n__from(X)) -> c_4(from#(X)) -->_1 from#(X) -> c_13(activate#(X),activate#(X)):7 4:S:activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)) -->_1 indx#(cons(X,Y),Z) -> c_16(activate#(X),activate#(Z),activate#(Y),activate#(Z)):8 -->_2 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_2 activate#(n__from(X)) -> c_4(from#(X)):3 -->_2 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_2 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 5:S:activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_1 sel#(0(),cons(X,Y)) -> c_20(activate#(X)):9 -->_3 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_2 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_3 activate#(n__from(X)) -> c_4(from#(X)):3 -->_2 activate#(n__from(X)) -> c_4(from#(X)):3 -->_3 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_2 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_3 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 -->_2 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 6:S:dbls#(cons(X,Y)) -> c_11(activate#(X),activate#(Y)) -->_2 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_1 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_2 activate#(n__from(X)) -> c_4(from#(X)):3 -->_1 activate#(n__from(X)) -> c_4(from#(X)):3 -->_2 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_1 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_2 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 -->_1 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 7:S:from#(X) -> c_13(activate#(X),activate#(X)) -->_2 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_1 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_2 activate#(n__from(X)) -> c_4(from#(X)):3 -->_1 activate#(n__from(X)) -> c_4(from#(X)):3 -->_2 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_1 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_2 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 -->_1 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 8:S:indx#(cons(X,Y),Z) -> c_16(activate#(X),activate#(Z),activate#(Y),activate#(Z)) -->_4 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_4 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_3 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_2 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_1 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_4 activate#(n__from(X)) -> c_4(from#(X)):3 -->_3 activate#(n__from(X)) -> c_4(from#(X)):3 -->_2 activate#(n__from(X)) -> c_4(from#(X)):3 -->_1 activate#(n__from(X)) -> c_4(from#(X)):3 -->_4 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_3 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_2 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_1 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_4 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 -->_3 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 -->_2 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 -->_1 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 9:S:sel#(0(),cons(X,Y)) -> c_20(activate#(X)) -->_1 activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)):4 -->_1 activate#(n__from(X)) -> c_4(from#(X)):3 -->_1 activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)):2 -->_1 activate#(n__dbl(X)) -> c_2(dbl#(activate(X)),activate#(X)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: activate#(n__dbl(X)) -> c_2(activate#(X)) * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: activate#(n__dbl(X)) -> c_2(activate#(X)) activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)) activate#(n__from(X)) -> c_4(from#(X)) activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)) activate#(n__sel(X1,X2)) -> c_7(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) dbls#(cons(X,Y)) -> c_11(activate#(X),activate#(Y)) from#(X) -> c_13(activate#(X),activate#(X)) indx#(cons(X,Y),Z) -> c_16(activate#(X),activate#(Z),activate#(Y),activate#(Z)) sel#(0(),cons(X,Y)) -> c_20(activate#(X)) - Weak TRS: activate(X) -> X activate(n__dbl(X)) -> dbl(activate(X)) activate(n__dbls(X)) -> dbls(activate(X)) activate(n__from(X)) -> from(X) activate(n__indx(X1,X2)) -> indx(activate(X1),X2) activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) dbl(X) -> n__dbl(X) dbl(0()) -> 0() dbls(X) -> n__dbls(X) dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y))) dbls(nil()) -> nil() from(X) -> cons(activate(X),n__from(n__s(activate(X)))) from(X) -> n__from(X) indx(X1,X2) -> n__indx(X1,X2) indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z))) indx(nil(),X) -> nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) sel(0(),cons(X,Y)) -> activate(X) - Signature: {activate/1,dbl/1,dbls/1,from/1,indx/2,s/1,sel/2,activate#/1,dbl#/1,dbls#/1,from#/1,indx#/2,s#/1 ,sel#/2} / {0/0,cons/2,n__dbl/1,n__dbls/1,n__from/1,n__indx/2,n__s/1,n__sel/2,nil/0,c_1/0,c_2/1,c_3/2,c_4/1 ,c_5/2,c_6/1,c_7/3,c_8/0,c_9/0,c_10/0,c_11/2,c_12/0,c_13/2,c_14/0,c_15/0,c_16/4,c_17/0,c_18/0,c_19/0,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,dbl#,dbls#,from#,indx#,s# ,sel#} and constructors {0,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE