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)))) dbl1(0()) -> 01() dbl1(s(X)) -> s1(s1(dbl1(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() quote(0()) -> 01() quote(dbl(X)) -> dbl1(X) quote(s(X)) -> s1(quote(activate(X))) quote(sel(X,Y)) -> sel1(X,Y) 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)) sel1(0(),cons(X,Y)) -> activate(X) sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z)) - Signature: {activate/1,dbl/1,dbl1/1,dbls/1,from/1,indx/2,quote/1,s/1,sel/2,sel1/2} / {0/0,01/0,cons/2,n__dbl/1 ,n__dbls/1,n__from/1,n__indx/2,n__s/1,n__sel/2,nil/0,s1/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,dbl,dbl1,dbls,from,indx,quote,s,sel ,sel1} and constructors {0,01,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil,s1} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. dbl(s(X)) -> s(n__s(n__dbl(activate(X)))) dbl1(s(X)) -> s1(s1(dbl1(activate(X)))) quote(dbl(X)) -> dbl1(X) quote(s(X)) -> s1(quote(activate(X))) quote(sel(X,Y)) -> sel1(X,Y) sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z)) sel1(s(X),cons(Y,Z)) -> sel1(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() dbl1(0()) -> 01() 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() quote(0()) -> 01() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) sel(0(),cons(X,Y)) -> activate(X) sel1(0(),cons(X,Y)) -> activate(X) - Signature: {activate/1,dbl/1,dbl1/1,dbls/1,from/1,indx/2,quote/1,s/1,sel/2,sel1/2} / {0/0,01/0,cons/2,n__dbl/1 ,n__dbls/1,n__from/1,n__indx/2,n__s/1,n__sel/2,nil/0,s1/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,dbl,dbl1,dbls,from,indx,quote,s,sel ,sel1} and constructors {0,01,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil,s1} + 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() dbl1#(0()) -> c_10() dbls#(X) -> c_11() dbls#(cons(X,Y)) -> c_12(activate#(X),activate#(Y)) dbls#(nil()) -> c_13() from#(X) -> c_14(activate#(X),activate#(X)) from#(X) -> c_15() indx#(X1,X2) -> c_16() indx#(cons(X,Y),Z) -> c_17(activate#(X),activate#(Z),activate#(Y),activate#(Z)) indx#(nil(),X) -> c_18() quote#(0()) -> c_19() s#(X) -> c_20() sel#(X1,X2) -> c_21() sel#(0(),cons(X,Y)) -> c_22(activate#(X)) sel1#(0(),cons(X,Y)) -> c_23(activate#(X)) Weak DPs and mark the set of starting terms. * Step 3: UsableRules 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() dbl1#(0()) -> c_10() dbls#(X) -> c_11() dbls#(cons(X,Y)) -> c_12(activate#(X),activate#(Y)) dbls#(nil()) -> c_13() from#(X) -> c_14(activate#(X),activate#(X)) from#(X) -> c_15() indx#(X1,X2) -> c_16() indx#(cons(X,Y),Z) -> c_17(activate#(X),activate#(Z),activate#(Y),activate#(Z)) indx#(nil(),X) -> c_18() quote#(0()) -> c_19() s#(X) -> c_20() sel#(X1,X2) -> c_21() sel#(0(),cons(X,Y)) -> c_22(activate#(X)) sel1#(0(),cons(X,Y)) -> c_23(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() dbl1(0()) -> 01() 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() quote(0()) -> 01() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) sel(0(),cons(X,Y)) -> activate(X) sel1(0(),cons(X,Y)) -> activate(X) - Signature: {activate/1,dbl/1,dbl1/1,dbls/1,from/1,indx/2,quote/1,s/1,sel/2,sel1/2,activate#/1,dbl#/1,dbl1#/1,dbls#/1 ,from#/1,indx#/2,quote#/1,s#/1,sel#/2,sel1#/2} / {0/0,01/0,cons/2,n__dbl/1,n__dbls/1,n__from/1,n__indx/2 ,n__s/1,n__sel/2,nil/0,s1/1,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/0,c_12/2 ,c_13/0,c_14/2,c_15/0,c_16/0,c_17/4,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,dbl#,dbl1#,dbls#,from#,indx#,quote#,s#,sel# ,sel1#} and constructors {0,01,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil,s1} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: 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) 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() dbl1#(0()) -> c_10() dbls#(X) -> c_11() dbls#(cons(X,Y)) -> c_12(activate#(X),activate#(Y)) dbls#(nil()) -> c_13() from#(X) -> c_14(activate#(X),activate#(X)) from#(X) -> c_15() indx#(X1,X2) -> c_16() indx#(cons(X,Y),Z) -> c_17(activate#(X),activate#(Z),activate#(Y),activate#(Z)) indx#(nil(),X) -> c_18() quote#(0()) -> c_19() s#(X) -> c_20() sel#(X1,X2) -> c_21() sel#(0(),cons(X,Y)) -> c_22(activate#(X)) sel1#(0(),cons(X,Y)) -> c_23(activate#(X)) * Step 4: 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() dbl1#(0()) -> c_10() dbls#(X) -> c_11() dbls#(cons(X,Y)) -> c_12(activate#(X),activate#(Y)) dbls#(nil()) -> c_13() from#(X) -> c_14(activate#(X),activate#(X)) from#(X) -> c_15() indx#(X1,X2) -> c_16() indx#(cons(X,Y),Z) -> c_17(activate#(X),activate#(Z),activate#(Y),activate#(Z)) indx#(nil(),X) -> c_18() quote#(0()) -> c_19() s#(X) -> c_20() sel#(X1,X2) -> c_21() sel#(0(),cons(X,Y)) -> c_22(activate#(X)) sel1#(0(),cons(X,Y)) -> c_23(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,dbl1/1,dbls/1,from/1,indx/2,quote/1,s/1,sel/2,sel1/2,activate#/1,dbl#/1,dbl1#/1,dbls#/1 ,from#/1,indx#/2,quote#/1,s#/1,sel#/2,sel1#/2} / {0/0,01/0,cons/2,n__dbl/1,n__dbls/1,n__from/1,n__indx/2 ,n__s/1,n__sel/2,nil/0,s1/1,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/0,c_12/2 ,c_13/0,c_14/2,c_15/0,c_16/0,c_17/4,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,dbl#,dbl1#,dbls#,from#,indx#,quote#,s#,sel# ,sel1#} and constructors {0,01,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil,s1} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,8,9,10,11,13,15,16,18,19,20,21} by application of Pre({1,8,9,10,11,13,15,16,18,19,20,21}) = {2,3,4,5,6,7,12,14,17,22,23}. 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: dbl1#(0()) -> c_10() 11: dbls#(X) -> c_11() 12: dbls#(cons(X,Y)) -> c_12(activate#(X),activate#(Y)) 13: dbls#(nil()) -> c_13() 14: from#(X) -> c_14(activate#(X),activate#(X)) 15: from#(X) -> c_15() 16: indx#(X1,X2) -> c_16() 17: indx#(cons(X,Y),Z) -> c_17(activate#(X),activate#(Z),activate#(Y),activate#(Z)) 18: indx#(nil(),X) -> c_18() 19: quote#(0()) -> c_19() 20: s#(X) -> c_20() 21: sel#(X1,X2) -> c_21() 22: sel#(0(),cons(X,Y)) -> c_22(activate#(X)) 23: sel1#(0(),cons(X,Y)) -> c_23(activate#(X)) * Step 5: 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_12(activate#(X),activate#(Y)) from#(X) -> c_14(activate#(X),activate#(X)) indx#(cons(X,Y),Z) -> c_17(activate#(X),activate#(Z),activate#(Y),activate#(Z)) sel#(0(),cons(X,Y)) -> c_22(activate#(X)) sel1#(0(),cons(X,Y)) -> c_23(activate#(X)) - Weak DPs: activate#(X) -> c_1() dbl#(X) -> c_8() dbl#(0()) -> c_9() dbl1#(0()) -> c_10() dbls#(X) -> c_11() dbls#(nil()) -> c_13() from#(X) -> c_15() indx#(X1,X2) -> c_16() indx#(nil(),X) -> c_18() quote#(0()) -> c_19() s#(X) -> c_20() sel#(X1,X2) -> c_21() - 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,dbl1/1,dbls/1,from/1,indx/2,quote/1,s/1,sel/2,sel1/2,activate#/1,dbl#/1,dbl1#/1,dbls#/1 ,from#/1,indx#/2,quote#/1,s#/1,sel#/2,sel1#/2} / {0/0,01/0,cons/2,n__dbl/1,n__dbls/1,n__from/1,n__indx/2 ,n__s/1,n__sel/2,nil/0,s1/1,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/0,c_12/2 ,c_13/0,c_14/2,c_15/0,c_16/0,c_17/4,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,dbl#,dbl1#,dbls#,from#,indx#,quote#,s#,sel# ,sel1#} and constructors {0,01,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil,s1} + 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,11}. 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_12(activate#(X),activate#(Y)) 8: from#(X) -> c_14(activate#(X),activate#(X)) 9: indx#(cons(X,Y),Z) -> c_17(activate#(X),activate#(Z),activate#(Y),activate#(Z)) 10: sel#(0(),cons(X,Y)) -> c_22(activate#(X)) 11: sel1#(0(),cons(X,Y)) -> c_23(activate#(X)) 12: activate#(X) -> c_1() 13: dbl#(X) -> c_8() 14: dbl#(0()) -> c_9() 15: dbl1#(0()) -> c_10() 16: dbls#(X) -> c_11() 17: dbls#(nil()) -> c_13() 18: from#(X) -> c_15() 19: indx#(X1,X2) -> c_16() 20: indx#(nil(),X) -> c_18() 21: quote#(0()) -> c_19() 22: s#(X) -> c_20() 23: sel#(X1,X2) -> c_21() * Step 6: 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_12(activate#(X),activate#(Y)) from#(X) -> c_14(activate#(X),activate#(X)) indx#(cons(X,Y),Z) -> c_17(activate#(X),activate#(Z),activate#(Y),activate#(Z)) sel#(0(),cons(X,Y)) -> c_22(activate#(X)) sel1#(0(),cons(X,Y)) -> c_23(activate#(X)) - Weak DPs: activate#(X) -> c_1() activate#(n__s(X)) -> c_6(s#(X)) dbl#(X) -> c_8() dbl#(0()) -> c_9() dbl1#(0()) -> c_10() dbls#(X) -> c_11() dbls#(nil()) -> c_13() from#(X) -> c_15() indx#(X1,X2) -> c_16() indx#(nil(),X) -> c_18() quote#(0()) -> c_19() s#(X) -> c_20() sel#(X1,X2) -> c_21() - 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,dbl1/1,dbls/1,from/1,indx/2,quote/1,s/1,sel/2,sel1/2,activate#/1,dbl#/1,dbl1#/1,dbls#/1 ,from#/1,indx#/2,quote#/1,s#/1,sel#/2,sel1#/2} / {0/0,01/0,cons/2,n__dbl/1,n__dbls/1,n__from/1,n__indx/2 ,n__s/1,n__sel/2,nil/0,s1/1,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/0,c_12/2 ,c_13/0,c_14/2,c_15/0,c_16/0,c_17/4,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,dbl#,dbl1#,dbls#,from#,indx#,quote#,s#,sel# ,sel1#} and constructors {0,01,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil,s1} + 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)):12 -->_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():14 -->_1 dbl#(X) -> c_8():13 -->_2 activate#(X) -> c_1():11 -->_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)):12 -->_1 dbls#(cons(X,Y)) -> c_12(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_13():17 -->_1 dbls#(X) -> c_11():16 -->_2 activate#(X) -> c_1():11 -->_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_14(activate#(X),activate#(X)):7 -->_1 from#(X) -> c_15():18 4:S:activate#(n__indx(X1,X2)) -> c_5(indx#(activate(X1),X2),activate#(X1)) -->_2 activate#(n__s(X)) -> c_6(s#(X)):12 -->_1 indx#(cons(X,Y),Z) -> c_17(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_18():20 -->_1 indx#(X1,X2) -> c_16():19 -->_2 activate#(X) -> c_1():11 -->_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)):12 -->_2 activate#(n__s(X)) -> c_6(s#(X)):12 -->_1 sel#(0(),cons(X,Y)) -> c_22(activate#(X)):9 -->_1 sel#(X1,X2) -> c_21():23 -->_3 activate#(X) -> c_1():11 -->_2 activate#(X) -> c_1():11 -->_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_12(activate#(X),activate#(Y)) -->_2 activate#(n__s(X)) -> c_6(s#(X)):12 -->_1 activate#(n__s(X)) -> c_6(s#(X)):12 -->_2 activate#(X) -> c_1():11 -->_1 activate#(X) -> c_1():11 -->_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_14(activate#(X),activate#(X)) -->_2 activate#(n__s(X)) -> c_6(s#(X)):12 -->_1 activate#(n__s(X)) -> c_6(s#(X)):12 -->_2 activate#(X) -> c_1():11 -->_1 activate#(X) -> c_1():11 -->_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_17(activate#(X),activate#(Z),activate#(Y),activate#(Z)) -->_4 activate#(n__s(X)) -> c_6(s#(X)):12 -->_3 activate#(n__s(X)) -> c_6(s#(X)):12 -->_2 activate#(n__s(X)) -> c_6(s#(X)):12 -->_1 activate#(n__s(X)) -> c_6(s#(X)):12 -->_4 activate#(X) -> c_1():11 -->_3 activate#(X) -> c_1():11 -->_2 activate#(X) -> c_1():11 -->_1 activate#(X) -> c_1():11 -->_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_22(activate#(X)) -->_1 activate#(n__s(X)) -> c_6(s#(X)):12 -->_1 activate#(X) -> c_1():11 -->_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:S:sel1#(0(),cons(X,Y)) -> c_23(activate#(X)) -->_1 activate#(n__s(X)) -> c_6(s#(X)):12 -->_1 activate#(X) -> c_1():11 -->_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 11:W:activate#(X) -> c_1() 12:W:activate#(n__s(X)) -> c_6(s#(X)) -->_1 s#(X) -> c_20():22 13:W:dbl#(X) -> c_8() 14:W:dbl#(0()) -> c_9() 15:W:dbl1#(0()) -> c_10() 16:W:dbls#(X) -> c_11() 17:W:dbls#(nil()) -> c_13() 18:W:from#(X) -> c_15() 19:W:indx#(X1,X2) -> c_16() 20:W:indx#(nil(),X) -> c_18() 21:W:quote#(0()) -> c_19() 22:W:s#(X) -> c_20() 23:W:sel#(X1,X2) -> c_21() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 21: quote#(0()) -> c_19() 15: dbl1#(0()) -> c_10() 13: dbl#(X) -> c_8() 14: dbl#(0()) -> c_9() 23: sel#(X1,X2) -> c_21() 19: indx#(X1,X2) -> c_16() 20: indx#(nil(),X) -> c_18() 18: from#(X) -> c_15() 16: dbls#(X) -> c_11() 17: dbls#(nil()) -> c_13() 11: activate#(X) -> c_1() 12: activate#(n__s(X)) -> c_6(s#(X)) 22: s#(X) -> c_20() * Step 7: 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_12(activate#(X),activate#(Y)) from#(X) -> c_14(activate#(X),activate#(X)) indx#(cons(X,Y),Z) -> c_17(activate#(X),activate#(Z),activate#(Y),activate#(Z)) sel#(0(),cons(X,Y)) -> c_22(activate#(X)) sel1#(0(),cons(X,Y)) -> c_23(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,dbl1/1,dbls/1,from/1,indx/2,quote/1,s/1,sel/2,sel1/2,activate#/1,dbl#/1,dbl1#/1,dbls#/1 ,from#/1,indx#/2,quote#/1,s#/1,sel#/2,sel1#/2} / {0/0,01/0,cons/2,n__dbl/1,n__dbls/1,n__from/1,n__indx/2 ,n__s/1,n__sel/2,nil/0,s1/1,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/0,c_12/2 ,c_13/0,c_14/2,c_15/0,c_16/0,c_17/4,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,dbl#,dbl1#,dbls#,from#,indx#,quote#,s#,sel# ,sel1#} and constructors {0,01,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil,s1} + 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_12(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_14(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_17(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_22(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_12(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_14(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_17(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_22(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 10:S:sel1#(0(),cons(X,Y)) -> c_23(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 8: RemoveHeads 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_12(activate#(X),activate#(Y)) from#(X) -> c_14(activate#(X),activate#(X)) indx#(cons(X,Y),Z) -> c_17(activate#(X),activate#(Z),activate#(Y),activate#(Z)) sel#(0(),cons(X,Y)) -> c_22(activate#(X)) sel1#(0(),cons(X,Y)) -> c_23(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,dbl1/1,dbls/1,from/1,indx/2,quote/1,s/1,sel/2,sel1/2,activate#/1,dbl#/1,dbl1#/1,dbls#/1 ,from#/1,indx#/2,quote#/1,s#/1,sel#/2,sel1#/2} / {0/0,01/0,cons/2,n__dbl/1,n__dbls/1,n__from/1,n__indx/2 ,n__s/1,n__sel/2,nil/0,s1/1,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/0,c_12/2 ,c_13/0,c_14/2,c_15/0,c_16/0,c_17/4,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,dbl#,dbl1#,dbls#,from#,indx#,quote#,s#,sel# ,sel1#} and constructors {0,01,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil,s1} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:activate#(n__dbl(X)) -> c_2(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(activate#(X)):1 2:S:activate#(n__dbls(X)) -> c_3(dbls#(activate(X)),activate#(X)) -->_1 dbls#(cons(X,Y)) -> c_12(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(activate#(X)):1 3:S:activate#(n__from(X)) -> c_4(from#(X)) -->_1 from#(X) -> c_14(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_17(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(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_22(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(activate#(X)):1 -->_2 activate#(n__dbl(X)) -> c_2(activate#(X)):1 6:S:dbls#(cons(X,Y)) -> c_12(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(activate#(X)):1 -->_1 activate#(n__dbl(X)) -> c_2(activate#(X)):1 7:S:from#(X) -> c_14(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(activate#(X)):1 -->_1 activate#(n__dbl(X)) -> c_2(activate#(X)):1 8:S:indx#(cons(X,Y),Z) -> c_17(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(activate#(X)):1 -->_3 activate#(n__dbl(X)) -> c_2(activate#(X)):1 -->_2 activate#(n__dbl(X)) -> c_2(activate#(X)):1 -->_1 activate#(n__dbl(X)) -> c_2(activate#(X)):1 9:S:sel#(0(),cons(X,Y)) -> c_22(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(activate#(X)):1 10:S:sel1#(0(),cons(X,Y)) -> c_23(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(activate#(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). [(10,sel1#(0(),cons(X,Y)) -> c_23(activate#(X)))] * Step 9: 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_12(activate#(X),activate#(Y)) from#(X) -> c_14(activate#(X),activate#(X)) indx#(cons(X,Y),Z) -> c_17(activate#(X),activate#(Z),activate#(Y),activate#(Z)) sel#(0(),cons(X,Y)) -> c_22(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,dbl1/1,dbls/1,from/1,indx/2,quote/1,s/1,sel/2,sel1/2,activate#/1,dbl#/1,dbl1#/1,dbls#/1 ,from#/1,indx#/2,quote#/1,s#/1,sel#/2,sel1#/2} / {0/0,01/0,cons/2,n__dbl/1,n__dbls/1,n__from/1,n__indx/2 ,n__s/1,n__sel/2,nil/0,s1/1,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/0,c_12/2 ,c_13/0,c_14/2,c_15/0,c_16/0,c_17/4,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,dbl#,dbl1#,dbls#,from#,indx#,quote#,s#,sel# ,sel1#} and constructors {0,01,cons,n__dbl,n__dbls,n__from,n__indx,n__s,n__sel,nil,s1} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE