WORST_CASE(?,O(n^1)) * Step 1: Sum. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: ACTIVATE(z0) -> c16() ACTIVATE(n__add(z0,z1)) -> c14(ADD(z0,z1)) ACTIVATE(n__from(z0)) -> c13(FROM(z0)) ACTIVATE(n__fst(z0,z1)) -> c12(FST(z0,z1)) ACTIVATE(n__len(z0)) -> c15(LEN(z0)) ADD(z0,z1) -> c8() ADD(0(),z0) -> c6() ADD(s(z0),z1) -> c7(ACTIVATE(z0)) FROM(z0) -> c4() FROM(z0) -> c5() FST(z0,z1) -> c3() FST(0(),z0) -> c() FST(s(z0),cons(z1,z2)) -> c1(ACTIVATE(z0)) FST(s(z0),cons(z1,z2)) -> c2(ACTIVATE(z2)) LEN(z0) -> c11() LEN(cons(z0,z1)) -> c10(ACTIVATE(z1)) LEN(nil()) -> c9() - Weak TRS: activate(z0) -> z0 activate(n__add(z0,z1)) -> add(z0,z1) activate(n__from(z0)) -> from(z0) activate(n__fst(z0,z1)) -> fst(z0,z1) activate(n__len(z0)) -> len(z0) add(z0,z1) -> n__add(z0,z1) add(0(),z0) -> z0 add(s(z0),z1) -> s(n__add(activate(z0),z1)) from(z0) -> cons(z0,n__from(s(z0))) from(z0) -> n__from(z0) fst(z0,z1) -> n__fst(z0,z1) fst(0(),z0) -> nil() fst(s(z0),cons(z1,z2)) -> cons(z1,n__fst(activate(z0),activate(z2))) len(z0) -> n__len(z0) len(cons(z0,z1)) -> s(n__len(activate(z1))) len(nil()) -> 0() - Signature: {ACTIVATE/1,ADD/2,FROM/1,FST/2,LEN/1,activate/1,add/2,from/1,fst/2,len/1} / {0/0,c/0,c1/1,c10/1,c11/0,c12/1 ,c13/1,c14/1,c15/1,c16/0,c2/1,c3/0,c4/0,c5/0,c6/0,c7/1,c8/0,c9/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1 ,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE,ADD,FROM,FST,LEN,activate,add,from,fst ,len} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__add,n__from ,n__fst,n__len,nil,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: ACTIVATE(z0) -> c16() ACTIVATE(n__add(z0,z1)) -> c14(ADD(z0,z1)) ACTIVATE(n__from(z0)) -> c13(FROM(z0)) ACTIVATE(n__fst(z0,z1)) -> c12(FST(z0,z1)) ACTIVATE(n__len(z0)) -> c15(LEN(z0)) ADD(z0,z1) -> c8() ADD(0(),z0) -> c6() ADD(s(z0),z1) -> c7(ACTIVATE(z0)) FROM(z0) -> c4() FROM(z0) -> c5() FST(z0,z1) -> c3() FST(0(),z0) -> c() FST(s(z0),cons(z1,z2)) -> c1(ACTIVATE(z0)) FST(s(z0),cons(z1,z2)) -> c2(ACTIVATE(z2)) LEN(z0) -> c11() LEN(cons(z0,z1)) -> c10(ACTIVATE(z1)) LEN(nil()) -> c9() - Weak TRS: activate(z0) -> z0 activate(n__add(z0,z1)) -> add(z0,z1) activate(n__from(z0)) -> from(z0) activate(n__fst(z0,z1)) -> fst(z0,z1) activate(n__len(z0)) -> len(z0) add(z0,z1) -> n__add(z0,z1) add(0(),z0) -> z0 add(s(z0),z1) -> s(n__add(activate(z0),z1)) from(z0) -> cons(z0,n__from(s(z0))) from(z0) -> n__from(z0) fst(z0,z1) -> n__fst(z0,z1) fst(0(),z0) -> nil() fst(s(z0),cons(z1,z2)) -> cons(z1,n__fst(activate(z0),activate(z2))) len(z0) -> n__len(z0) len(cons(z0,z1)) -> s(n__len(activate(z1))) len(nil()) -> 0() - Signature: {ACTIVATE/1,ADD/2,FROM/1,FST/2,LEN/1,activate/1,add/2,from/1,fst/2,len/1} / {0/0,c/0,c1/1,c10/1,c11/0,c12/1 ,c13/1,c14/1,c15/1,c16/0,c2/1,c3/0,c4/0,c5/0,c6/0,c7/1,c8/0,c9/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1 ,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE,ADD,FROM,FST,LEN,activate,add,from,fst ,len} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__add,n__from ,n__fst,n__len,nil,s} + Applied Processor: DependencyPairs {dpKind_ = WIDP} + Details: We add the following weak innermost dependency pairs: Strict DPs ACTIVATE#(z0) -> c_1() ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) ACTIVATE#(n__from(z0)) -> c_3(FROM#(z0)) ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) ADD#(z0,z1) -> c_6() ADD#(0(),z0) -> c_7() ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) FROM#(z0) -> c_9() FROM#(z0) -> c_10() FST#(z0,z1) -> c_11() FST#(0(),z0) -> c_12() FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) LEN#(z0) -> c_15() LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) LEN#(nil()) -> c_17() Weak DPs activate#(z0) -> c_18() activate#(n__add(z0,z1)) -> c_19(add#(z0,z1)) activate#(n__from(z0)) -> c_20(from#(z0)) activate#(n__fst(z0,z1)) -> c_21(fst#(z0,z1)) activate#(n__len(z0)) -> c_22(len#(z0)) add#(z0,z1) -> c_23() add#(0(),z0) -> c_24() add#(s(z0),z1) -> c_25(activate#(z0)) from#(z0) -> c_26() from#(z0) -> c_27() fst#(z0,z1) -> c_28() fst#(0(),z0) -> c_29() fst#(s(z0),cons(z1,z2)) -> c_30(activate#(z0),activate#(z2)) len#(z0) -> c_31() len#(cons(z0,z1)) -> c_32(activate#(z1)) len#(nil()) -> c_33() and mark the set of starting terms. * Step 3: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ACTIVATE#(z0) -> c_1() ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) ACTIVATE#(n__from(z0)) -> c_3(FROM#(z0)) ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) ADD#(z0,z1) -> c_6() ADD#(0(),z0) -> c_7() ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) FROM#(z0) -> c_9() FROM#(z0) -> c_10() FST#(z0,z1) -> c_11() FST#(0(),z0) -> c_12() FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) LEN#(z0) -> c_15() LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) LEN#(nil()) -> c_17() - Strict TRS: ACTIVATE(z0) -> c16() ACTIVATE(n__add(z0,z1)) -> c14(ADD(z0,z1)) ACTIVATE(n__from(z0)) -> c13(FROM(z0)) ACTIVATE(n__fst(z0,z1)) -> c12(FST(z0,z1)) ACTIVATE(n__len(z0)) -> c15(LEN(z0)) ADD(z0,z1) -> c8() ADD(0(),z0) -> c6() ADD(s(z0),z1) -> c7(ACTIVATE(z0)) FROM(z0) -> c4() FROM(z0) -> c5() FST(z0,z1) -> c3() FST(0(),z0) -> c() FST(s(z0),cons(z1,z2)) -> c1(ACTIVATE(z0)) FST(s(z0),cons(z1,z2)) -> c2(ACTIVATE(z2)) LEN(z0) -> c11() LEN(cons(z0,z1)) -> c10(ACTIVATE(z1)) LEN(nil()) -> c9() - Weak DPs: activate#(z0) -> c_18() activate#(n__add(z0,z1)) -> c_19(add#(z0,z1)) activate#(n__from(z0)) -> c_20(from#(z0)) activate#(n__fst(z0,z1)) -> c_21(fst#(z0,z1)) activate#(n__len(z0)) -> c_22(len#(z0)) add#(z0,z1) -> c_23() add#(0(),z0) -> c_24() add#(s(z0),z1) -> c_25(activate#(z0)) from#(z0) -> c_26() from#(z0) -> c_27() fst#(z0,z1) -> c_28() fst#(0(),z0) -> c_29() fst#(s(z0),cons(z1,z2)) -> c_30(activate#(z0),activate#(z2)) len#(z0) -> c_31() len#(cons(z0,z1)) -> c_32(activate#(z1)) len#(nil()) -> c_33() - Weak TRS: activate(z0) -> z0 activate(n__add(z0,z1)) -> add(z0,z1) activate(n__from(z0)) -> from(z0) activate(n__fst(z0,z1)) -> fst(z0,z1) activate(n__len(z0)) -> len(z0) add(z0,z1) -> n__add(z0,z1) add(0(),z0) -> z0 add(s(z0),z1) -> s(n__add(activate(z0),z1)) from(z0) -> cons(z0,n__from(s(z0))) from(z0) -> n__from(z0) fst(z0,z1) -> n__fst(z0,z1) fst(0(),z0) -> nil() fst(s(z0),cons(z1,z2)) -> cons(z1,n__fst(activate(z0),activate(z2))) len(z0) -> n__len(z0) len(cons(z0,z1)) -> s(n__len(activate(z1))) len(nil()) -> 0() - Signature: {ACTIVATE/1,ADD/2,FROM/1,FST/2,LEN/1,activate/1,add/2,from/1,fst/2,len/1,ACTIVATE#/1,ADD#/2,FROM#/1,FST#/2 ,LEN#/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/1,c15/1,c16/0 ,c2/1,c3/0,c4/0,c5/0,c6/0,c7/1,c8/0,c9/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/0 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/0,c_30/2,c_31/0,c_32/1,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,FROM#,FST#,LEN#,activate#,add#,from#,fst# ,len#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__add,n__from ,n__fst,n__len,nil,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: ACTIVATE#(z0) -> c_1() ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) ACTIVATE#(n__from(z0)) -> c_3(FROM#(z0)) ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) ADD#(z0,z1) -> c_6() ADD#(0(),z0) -> c_7() ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) FROM#(z0) -> c_9() FROM#(z0) -> c_10() FST#(z0,z1) -> c_11() FST#(0(),z0) -> c_12() FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) LEN#(z0) -> c_15() LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) LEN#(nil()) -> c_17() activate#(z0) -> c_18() activate#(n__add(z0,z1)) -> c_19(add#(z0,z1)) activate#(n__from(z0)) -> c_20(from#(z0)) activate#(n__fst(z0,z1)) -> c_21(fst#(z0,z1)) activate#(n__len(z0)) -> c_22(len#(z0)) add#(z0,z1) -> c_23() add#(0(),z0) -> c_24() add#(s(z0),z1) -> c_25(activate#(z0)) from#(z0) -> c_26() from#(z0) -> c_27() fst#(z0,z1) -> c_28() fst#(0(),z0) -> c_29() fst#(s(z0),cons(z1,z2)) -> c_30(activate#(z0),activate#(z2)) len#(z0) -> c_31() len#(cons(z0,z1)) -> c_32(activate#(z1)) len#(nil()) -> c_33() * Step 4: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ACTIVATE#(z0) -> c_1() ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) ACTIVATE#(n__from(z0)) -> c_3(FROM#(z0)) ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) ADD#(z0,z1) -> c_6() ADD#(0(),z0) -> c_7() ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) FROM#(z0) -> c_9() FROM#(z0) -> c_10() FST#(z0,z1) -> c_11() FST#(0(),z0) -> c_12() FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) LEN#(z0) -> c_15() LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) LEN#(nil()) -> c_17() - Weak DPs: activate#(z0) -> c_18() activate#(n__add(z0,z1)) -> c_19(add#(z0,z1)) activate#(n__from(z0)) -> c_20(from#(z0)) activate#(n__fst(z0,z1)) -> c_21(fst#(z0,z1)) activate#(n__len(z0)) -> c_22(len#(z0)) add#(z0,z1) -> c_23() add#(0(),z0) -> c_24() add#(s(z0),z1) -> c_25(activate#(z0)) from#(z0) -> c_26() from#(z0) -> c_27() fst#(z0,z1) -> c_28() fst#(0(),z0) -> c_29() fst#(s(z0),cons(z1,z2)) -> c_30(activate#(z0),activate#(z2)) len#(z0) -> c_31() len#(cons(z0,z1)) -> c_32(activate#(z1)) len#(nil()) -> c_33() - Signature: {ACTIVATE/1,ADD/2,FROM/1,FST/2,LEN/1,activate/1,add/2,from/1,fst/2,len/1,ACTIVATE#/1,ADD#/2,FROM#/1,FST#/2 ,LEN#/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/1,c15/1,c16/0 ,c2/1,c3/0,c4/0,c5/0,c6/0,c7/1,c8/0,c9/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/0 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/0,c_30/2,c_31/0,c_32/1,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,FROM#,FST#,LEN#,activate#,add#,from#,fst# ,len#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__add,n__from ,n__fst,n__len,nil,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,6,7,9,10,11,12,15,17} by application of Pre({1,6,7,9,10,11,12,15,17}) = {2,3,4,5,8,13,14,16}. Here rules are labelled as follows: 1: ACTIVATE#(z0) -> c_1() 2: ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) 3: ACTIVATE#(n__from(z0)) -> c_3(FROM#(z0)) 4: ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) 5: ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) 6: ADD#(z0,z1) -> c_6() 7: ADD#(0(),z0) -> c_7() 8: ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) 9: FROM#(z0) -> c_9() 10: FROM#(z0) -> c_10() 11: FST#(z0,z1) -> c_11() 12: FST#(0(),z0) -> c_12() 13: FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) 14: FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) 15: LEN#(z0) -> c_15() 16: LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) 17: LEN#(nil()) -> c_17() 18: activate#(z0) -> c_18() 19: activate#(n__add(z0,z1)) -> c_19(add#(z0,z1)) 20: activate#(n__from(z0)) -> c_20(from#(z0)) 21: activate#(n__fst(z0,z1)) -> c_21(fst#(z0,z1)) 22: activate#(n__len(z0)) -> c_22(len#(z0)) 23: add#(z0,z1) -> c_23() 24: add#(0(),z0) -> c_24() 25: add#(s(z0),z1) -> c_25(activate#(z0)) 26: from#(z0) -> c_26() 27: from#(z0) -> c_27() 28: fst#(z0,z1) -> c_28() 29: fst#(0(),z0) -> c_29() 30: fst#(s(z0),cons(z1,z2)) -> c_30(activate#(z0),activate#(z2)) 31: len#(z0) -> c_31() 32: len#(cons(z0,z1)) -> c_32(activate#(z1)) 33: len#(nil()) -> c_33() * Step 5: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) ACTIVATE#(n__from(z0)) -> c_3(FROM#(z0)) ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) - Weak DPs: ACTIVATE#(z0) -> c_1() ADD#(z0,z1) -> c_6() ADD#(0(),z0) -> c_7() FROM#(z0) -> c_9() FROM#(z0) -> c_10() FST#(z0,z1) -> c_11() FST#(0(),z0) -> c_12() LEN#(z0) -> c_15() LEN#(nil()) -> c_17() activate#(z0) -> c_18() activate#(n__add(z0,z1)) -> c_19(add#(z0,z1)) activate#(n__from(z0)) -> c_20(from#(z0)) activate#(n__fst(z0,z1)) -> c_21(fst#(z0,z1)) activate#(n__len(z0)) -> c_22(len#(z0)) add#(z0,z1) -> c_23() add#(0(),z0) -> c_24() add#(s(z0),z1) -> c_25(activate#(z0)) from#(z0) -> c_26() from#(z0) -> c_27() fst#(z0,z1) -> c_28() fst#(0(),z0) -> c_29() fst#(s(z0),cons(z1,z2)) -> c_30(activate#(z0),activate#(z2)) len#(z0) -> c_31() len#(cons(z0,z1)) -> c_32(activate#(z1)) len#(nil()) -> c_33() - Signature: {ACTIVATE/1,ADD/2,FROM/1,FST/2,LEN/1,activate/1,add/2,from/1,fst/2,len/1,ACTIVATE#/1,ADD#/2,FROM#/1,FST#/2 ,LEN#/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/1,c15/1,c16/0 ,c2/1,c3/0,c4/0,c5/0,c6/0,c7/1,c8/0,c9/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/0 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/0,c_30/2,c_31/0,c_32/1,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,FROM#,FST#,LEN#,activate#,add#,from#,fst# ,len#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__add,n__from ,n__fst,n__len,nil,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2} by application of Pre({2}) = {5,6,7,8}. Here rules are labelled as follows: 1: ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) 2: ACTIVATE#(n__from(z0)) -> c_3(FROM#(z0)) 3: ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) 4: ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) 5: ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) 6: FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) 7: FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) 8: LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) 9: ACTIVATE#(z0) -> c_1() 10: ADD#(z0,z1) -> c_6() 11: ADD#(0(),z0) -> c_7() 12: FROM#(z0) -> c_9() 13: FROM#(z0) -> c_10() 14: FST#(z0,z1) -> c_11() 15: FST#(0(),z0) -> c_12() 16: LEN#(z0) -> c_15() 17: LEN#(nil()) -> c_17() 18: activate#(z0) -> c_18() 19: activate#(n__add(z0,z1)) -> c_19(add#(z0,z1)) 20: activate#(n__from(z0)) -> c_20(from#(z0)) 21: activate#(n__fst(z0,z1)) -> c_21(fst#(z0,z1)) 22: activate#(n__len(z0)) -> c_22(len#(z0)) 23: add#(z0,z1) -> c_23() 24: add#(0(),z0) -> c_24() 25: add#(s(z0),z1) -> c_25(activate#(z0)) 26: from#(z0) -> c_26() 27: from#(z0) -> c_27() 28: fst#(z0,z1) -> c_28() 29: fst#(0(),z0) -> c_29() 30: fst#(s(z0),cons(z1,z2)) -> c_30(activate#(z0),activate#(z2)) 31: len#(z0) -> c_31() 32: len#(cons(z0,z1)) -> c_32(activate#(z1)) 33: len#(nil()) -> c_33() * Step 6: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) - Weak DPs: ACTIVATE#(z0) -> c_1() ACTIVATE#(n__from(z0)) -> c_3(FROM#(z0)) ADD#(z0,z1) -> c_6() ADD#(0(),z0) -> c_7() FROM#(z0) -> c_9() FROM#(z0) -> c_10() FST#(z0,z1) -> c_11() FST#(0(),z0) -> c_12() LEN#(z0) -> c_15() LEN#(nil()) -> c_17() activate#(z0) -> c_18() activate#(n__add(z0,z1)) -> c_19(add#(z0,z1)) activate#(n__from(z0)) -> c_20(from#(z0)) activate#(n__fst(z0,z1)) -> c_21(fst#(z0,z1)) activate#(n__len(z0)) -> c_22(len#(z0)) add#(z0,z1) -> c_23() add#(0(),z0) -> c_24() add#(s(z0),z1) -> c_25(activate#(z0)) from#(z0) -> c_26() from#(z0) -> c_27() fst#(z0,z1) -> c_28() fst#(0(),z0) -> c_29() fst#(s(z0),cons(z1,z2)) -> c_30(activate#(z0),activate#(z2)) len#(z0) -> c_31() len#(cons(z0,z1)) -> c_32(activate#(z1)) len#(nil()) -> c_33() - Signature: {ACTIVATE/1,ADD/2,FROM/1,FST/2,LEN/1,activate/1,add/2,from/1,fst/2,len/1,ACTIVATE#/1,ADD#/2,FROM#/1,FST#/2 ,LEN#/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/1,c15/1,c16/0 ,c2/1,c3/0,c4/0,c5/0,c6/0,c7/1,c8/0,c9/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/0 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/0,c_30/2,c_31/0,c_32/1,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,FROM#,FST#,LEN#,activate#,add#,from#,fst# ,len#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__add,n__from ,n__fst,n__len,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) -->_1 ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)):4 -->_1 ADD#(0(),z0) -> c_7():11 -->_1 ADD#(z0,z1) -> c_6():10 2:S:ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) -->_1 FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)):6 -->_1 FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)):5 -->_1 FST#(0(),z0) -> c_12():15 -->_1 FST#(z0,z1) -> c_11():14 3:S:ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) -->_1 LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)):7 -->_1 LEN#(nil()) -> c_17():17 -->_1 LEN#(z0) -> c_15():16 4:S:ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) -->_1 ACTIVATE#(n__from(z0)) -> c_3(FROM#(z0)):9 -->_1 ACTIVATE#(z0) -> c_1():8 -->_1 ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)):3 -->_1 ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)):2 -->_1 ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)):1 5:S:FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) -->_1 ACTIVATE#(n__from(z0)) -> c_3(FROM#(z0)):9 -->_1 ACTIVATE#(z0) -> c_1():8 -->_1 ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)):3 -->_1 ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)):2 -->_1 ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)):1 6:S:FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) -->_1 ACTIVATE#(n__from(z0)) -> c_3(FROM#(z0)):9 -->_1 ACTIVATE#(z0) -> c_1():8 -->_1 ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)):3 -->_1 ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)):2 -->_1 ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)):1 7:S:LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) -->_1 ACTIVATE#(n__from(z0)) -> c_3(FROM#(z0)):9 -->_1 ACTIVATE#(z0) -> c_1():8 -->_1 ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)):3 -->_1 ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)):2 -->_1 ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)):1 8:W:ACTIVATE#(z0) -> c_1() 9:W:ACTIVATE#(n__from(z0)) -> c_3(FROM#(z0)) -->_1 FROM#(z0) -> c_10():13 -->_1 FROM#(z0) -> c_9():12 10:W:ADD#(z0,z1) -> c_6() 11:W:ADD#(0(),z0) -> c_7() 12:W:FROM#(z0) -> c_9() 13:W:FROM#(z0) -> c_10() 14:W:FST#(z0,z1) -> c_11() 15:W:FST#(0(),z0) -> c_12() 16:W:LEN#(z0) -> c_15() 17:W:LEN#(nil()) -> c_17() 18:W:activate#(z0) -> c_18() 19:W:activate#(n__add(z0,z1)) -> c_19(add#(z0,z1)) -->_1 add#(s(z0),z1) -> c_25(activate#(z0)):25 -->_1 add#(0(),z0) -> c_24():24 -->_1 add#(z0,z1) -> c_23():23 20:W:activate#(n__from(z0)) -> c_20(from#(z0)) -->_1 from#(z0) -> c_27():27 -->_1 from#(z0) -> c_26():26 21:W:activate#(n__fst(z0,z1)) -> c_21(fst#(z0,z1)) -->_1 fst#(s(z0),cons(z1,z2)) -> c_30(activate#(z0),activate#(z2)):30 -->_1 fst#(0(),z0) -> c_29():29 -->_1 fst#(z0,z1) -> c_28():28 22:W:activate#(n__len(z0)) -> c_22(len#(z0)) -->_1 len#(cons(z0,z1)) -> c_32(activate#(z1)):32 -->_1 len#(nil()) -> c_33():33 -->_1 len#(z0) -> c_31():31 23:W:add#(z0,z1) -> c_23() 24:W:add#(0(),z0) -> c_24() 25:W:add#(s(z0),z1) -> c_25(activate#(z0)) -->_1 activate#(n__len(z0)) -> c_22(len#(z0)):22 -->_1 activate#(n__fst(z0,z1)) -> c_21(fst#(z0,z1)):21 -->_1 activate#(n__from(z0)) -> c_20(from#(z0)):20 -->_1 activate#(n__add(z0,z1)) -> c_19(add#(z0,z1)):19 -->_1 activate#(z0) -> c_18():18 26:W:from#(z0) -> c_26() 27:W:from#(z0) -> c_27() 28:W:fst#(z0,z1) -> c_28() 29:W:fst#(0(),z0) -> c_29() 30:W:fst#(s(z0),cons(z1,z2)) -> c_30(activate#(z0),activate#(z2)) -->_2 activate#(n__len(z0)) -> c_22(len#(z0)):22 -->_1 activate#(n__len(z0)) -> c_22(len#(z0)):22 -->_2 activate#(n__fst(z0,z1)) -> c_21(fst#(z0,z1)):21 -->_1 activate#(n__fst(z0,z1)) -> c_21(fst#(z0,z1)):21 -->_2 activate#(n__from(z0)) -> c_20(from#(z0)):20 -->_1 activate#(n__from(z0)) -> c_20(from#(z0)):20 -->_2 activate#(n__add(z0,z1)) -> c_19(add#(z0,z1)):19 -->_1 activate#(n__add(z0,z1)) -> c_19(add#(z0,z1)):19 -->_2 activate#(z0) -> c_18():18 -->_1 activate#(z0) -> c_18():18 31:W:len#(z0) -> c_31() 32:W:len#(cons(z0,z1)) -> c_32(activate#(z1)) -->_1 activate#(n__len(z0)) -> c_22(len#(z0)):22 -->_1 activate#(n__fst(z0,z1)) -> c_21(fst#(z0,z1)):21 -->_1 activate#(n__from(z0)) -> c_20(from#(z0)):20 -->_1 activate#(n__add(z0,z1)) -> c_19(add#(z0,z1)):19 -->_1 activate#(z0) -> c_18():18 33:W:len#(nil()) -> c_33() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 19: activate#(n__add(z0,z1)) -> c_19(add#(z0,z1)) 32: len#(cons(z0,z1)) -> c_32(activate#(z1)) 22: activate#(n__len(z0)) -> c_22(len#(z0)) 30: fst#(s(z0),cons(z1,z2)) -> c_30(activate#(z0),activate#(z2)) 21: activate#(n__fst(z0,z1)) -> c_21(fst#(z0,z1)) 25: add#(s(z0),z1) -> c_25(activate#(z0)) 23: add#(z0,z1) -> c_23() 24: add#(0(),z0) -> c_24() 31: len#(z0) -> c_31() 33: len#(nil()) -> c_33() 28: fst#(z0,z1) -> c_28() 29: fst#(0(),z0) -> c_29() 20: activate#(n__from(z0)) -> c_20(from#(z0)) 26: from#(z0) -> c_26() 27: from#(z0) -> c_27() 18: activate#(z0) -> c_18() 10: ADD#(z0,z1) -> c_6() 11: ADD#(0(),z0) -> c_7() 16: LEN#(z0) -> c_15() 17: LEN#(nil()) -> c_17() 14: FST#(z0,z1) -> c_11() 15: FST#(0(),z0) -> c_12() 8: ACTIVATE#(z0) -> c_1() 9: ACTIVATE#(n__from(z0)) -> c_3(FROM#(z0)) 12: FROM#(z0) -> c_9() 13: FROM#(z0) -> c_10() * Step 7: PredecessorEstimationCP. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) - Signature: {ACTIVATE/1,ADD/2,FROM/1,FST/2,LEN/1,activate/1,add/2,from/1,fst/2,len/1,ACTIVATE#/1,ADD#/2,FROM#/1,FST#/2 ,LEN#/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/1,c15/1,c16/0 ,c2/1,c3/0,c4/0,c5/0,c6/0,c7/1,c8/0,c9/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/0 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/0,c_30/2,c_31/0,c_32/1,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,FROM#,FST#,LEN#,activate#,add#,from#,fst# ,len#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__add,n__from ,n__fst,n__len,nil,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) 4: ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) 5: FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) 6: FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) 7: LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) Consider the set of all dependency pairs 1: ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) 2: ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) 3: ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) 4: ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) 5: FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) 6: FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) 7: LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1)) BEST_CASE TIME (?,?) SPACE(?,?)on application of the dependency pairs {2,4,5,6,7} These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5,6,7} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. ** Step 7.a:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) - Signature: {ACTIVATE/1,ADD/2,FROM/1,FST/2,LEN/1,activate/1,add/2,from/1,fst/2,len/1,ACTIVATE#/1,ADD#/2,FROM#/1,FST#/2 ,LEN#/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/1,c15/1,c16/0 ,c2/1,c3/0,c4/0,c5/0,c6/0,c7/1,c8/0,c9/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/0 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/0,c_30/2,c_31/0,c_32/1,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,FROM#,FST#,LEN#,activate#,add#,from#,fst# ,len#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__add,n__from ,n__fst,n__len,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_8) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1} Following symbols are considered usable: {ACTIVATE#,ADD#,FROM#,FST#,LEN#,activate#,add#,from#,fst#,len#} TcT has computed the following interpretation: p(0) = [1] p(ACTIVATE) = [1] x1 + [1] p(ADD) = [1] x1 + [1] p(FROM) = [0] p(FST) = [1] x2 + [1] p(LEN) = [1] x1 + [2] p(activate) = [8] x1 + [4] p(add) = [1] p(c) = [1] p(c1) = [2] p(c10) = [1] x1 + [0] p(c11) = [1] p(c12) = [1] x1 + [0] p(c13) = [0] p(c14) = [2] p(c15) = [1] p(c16) = [4] p(c2) = [1] x1 + [1] p(c3) = [1] p(c4) = [0] p(c5) = [1] p(c6) = [0] p(c7) = [0] p(c8) = [1] p(c9) = [1] p(cons) = [1] x2 + [2] p(from) = [1] x1 + [1] p(fst) = [1] x1 + [1] x2 + [4] p(len) = [1] x1 + [1] p(n__add) = [1] x1 + [0] p(n__from) = [1] p(n__fst) = [1] x1 + [1] x2 + [4] p(n__len) = [1] x1 + [4] p(nil) = [0] p(s) = [1] x1 + [2] p(ACTIVATE#) = [4] x1 + [0] p(ADD#) = [4] x1 + [0] p(FROM#) = [1] x1 + [1] p(FST#) = [4] x1 + [4] x2 + [0] p(LEN#) = [4] x1 + [10] p(activate#) = [2] p(add#) = [1] x2 + [1] p(from#) = [1] x1 + [2] p(fst#) = [4] x2 + [0] p(len#) = [2] x1 + [1] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [4] x1 + [0] p(c_4) = [1] x1 + [15] p(c_5) = [1] x1 + [6] p(c_6) = [0] p(c_7) = [0] p(c_8) = [1] x1 + [5] p(c_9) = [0] p(c_10) = [1] p(c_11) = [2] p(c_12) = [0] p(c_13) = [1] x1 + [8] p(c_14) = [1] x1 + [15] p(c_15) = [0] p(c_16) = [1] x1 + [1] p(c_17) = [8] p(c_18) = [1] p(c_19) = [2] p(c_20) = [1] x1 + [0] p(c_21) = [1] p(c_22) = [0] p(c_23) = [4] p(c_24) = [8] p(c_25) = [2] x1 + [0] p(c_26) = [1] p(c_27) = [1] p(c_28) = [2] p(c_29) = [0] p(c_30) = [0] p(c_31) = [1] p(c_32) = [1] x1 + [2] p(c_33) = [2] Following rules are strictly oriented: ACTIVATE#(n__fst(z0,z1)) = [4] z0 + [4] z1 + [16] > [4] z0 + [4] z1 + [15] = c_4(FST#(z0,z1)) ADD#(s(z0),z1) = [4] z0 + [8] > [4] z0 + [5] = c_8(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) = [4] z0 + [4] z2 + [16] > [4] z0 + [8] = c_13(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) = [4] z0 + [4] z2 + [16] > [4] z2 + [15] = c_14(ACTIVATE#(z2)) LEN#(cons(z0,z1)) = [4] z1 + [18] > [4] z1 + [1] = c_16(ACTIVATE#(z1)) Following rules are (at-least) weakly oriented: ACTIVATE#(n__add(z0,z1)) = [4] z0 + [0] >= [4] z0 + [0] = c_2(ADD#(z0,z1)) ACTIVATE#(n__len(z0)) = [4] z0 + [16] >= [4] z0 + [16] = c_5(LEN#(z0)) ** Step 7.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) - Weak DPs: ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) - Signature: {ACTIVATE/1,ADD/2,FROM/1,FST/2,LEN/1,activate/1,add/2,from/1,fst/2,len/1,ACTIVATE#/1,ADD#/2,FROM#/1,FST#/2 ,LEN#/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/1,c15/1,c16/0 ,c2/1,c3/0,c4/0,c5/0,c6/0,c7/1,c8/0,c9/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/0 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/0,c_30/2,c_31/0,c_32/1,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,FROM#,FST#,LEN#,activate#,add#,from#,fst# ,len#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__add,n__from ,n__fst,n__len,nil,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () ** Step 7.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) - Signature: {ACTIVATE/1,ADD/2,FROM/1,FST/2,LEN/1,activate/1,add/2,from/1,fst/2,len/1,ACTIVATE#/1,ADD#/2,FROM#/1,FST#/2 ,LEN#/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/1,c15/1,c16/0 ,c2/1,c3/0,c4/0,c5/0,c6/0,c7/1,c8/0,c9/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/0 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/0,c_30/2,c_31/0,c_32/1,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,FROM#,FST#,LEN#,activate#,add#,from#,fst# ,len#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__add,n__from ,n__fst,n__len,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) -->_1 ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)):4 2:W:ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) -->_1 FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)):6 -->_1 FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)):5 3:W:ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) -->_1 LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)):7 4:W:ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) -->_1 ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)):3 -->_1 ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)):2 -->_1 ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)):1 5:W:FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) -->_1 ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)):3 -->_1 ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)):2 -->_1 ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)):1 6:W:FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) -->_1 ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)):3 -->_1 ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)):2 -->_1 ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)):1 7:W:LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) -->_1 ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)):3 -->_1 ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)):2 -->_1 ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: ACTIVATE#(n__add(z0,z1)) -> c_2(ADD#(z0,z1)) 7: LEN#(cons(z0,z1)) -> c_16(ACTIVATE#(z1)) 3: ACTIVATE#(n__len(z0)) -> c_5(LEN#(z0)) 6: FST#(s(z0),cons(z1,z2)) -> c_14(ACTIVATE#(z2)) 2: ACTIVATE#(n__fst(z0,z1)) -> c_4(FST#(z0,z1)) 5: FST#(s(z0),cons(z1,z2)) -> c_13(ACTIVATE#(z0)) 4: ADD#(s(z0),z1) -> c_8(ACTIVATE#(z0)) ** Step 7.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Signature: {ACTIVATE/1,ADD/2,FROM/1,FST/2,LEN/1,activate/1,add/2,from/1,fst/2,len/1,ACTIVATE#/1,ADD#/2,FROM#/1,FST#/2 ,LEN#/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/1,c15/1,c16/0 ,c2/1,c3/0,c4/0,c5/0,c6/0,c7/1,c8/0,c9/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/0 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/0,c_30/2,c_31/0,c_32/1,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,FROM#,FST#,LEN#,activate#,add#,from#,fst# ,len#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__add,n__from ,n__fst,n__len,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))