WORST_CASE(Omega(n^1),O(n^3)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^3)) + Considered Problem: - Strict TRS: ACTIVATE(z0) -> c14() ACTIVATE(n__first(z0,z1)) -> c13(FIRST(z0,z1)) ACTIVATE(n__terms(z0)) -> c12(TERMS(z0)) ADD(0(),z0) -> c7() ADD(s(z0),z1) -> c8(ADD(z0,z1)) DBL(0()) -> c5() DBL(s(z0)) -> c6(DBL(z0)) FIRST(z0,z1) -> c11() FIRST(0(),z0) -> c9() FIRST(s(z0),cons(z1,z2)) -> c10(ACTIVATE(z2)) SQR(0()) -> c2() SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c4(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(SQR(z0)) TERMS(z0) -> c1() - Weak TRS: activate(z0) -> z0 activate(n__first(z0,z1)) -> first(z0,z1) activate(n__terms(z0)) -> terms(z0) add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) first(z0,z1) -> n__first(z0,z1) first(0(),z0) -> nil() first(s(z0),cons(z1,z2)) -> cons(z1,n__first(z0,activate(z2))) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0)),n__terms(s(z0))) terms(z0) -> n__terms(z0) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE,ADD,DBL,FIRST,SQR,TERMS,activate,add,dbl,first ,sqr,terms} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first,n__terms,nil ,recip,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: ACTIVATE(z0) -> c14() ACTIVATE(n__first(z0,z1)) -> c13(FIRST(z0,z1)) ACTIVATE(n__terms(z0)) -> c12(TERMS(z0)) ADD(0(),z0) -> c7() ADD(s(z0),z1) -> c8(ADD(z0,z1)) DBL(0()) -> c5() DBL(s(z0)) -> c6(DBL(z0)) FIRST(z0,z1) -> c11() FIRST(0(),z0) -> c9() FIRST(s(z0),cons(z1,z2)) -> c10(ACTIVATE(z2)) SQR(0()) -> c2() SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c4(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(SQR(z0)) TERMS(z0) -> c1() - Weak TRS: activate(z0) -> z0 activate(n__first(z0,z1)) -> first(z0,z1) activate(n__terms(z0)) -> terms(z0) add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) first(z0,z1) -> n__first(z0,z1) first(0(),z0) -> nil() first(s(z0),cons(z1,z2)) -> cons(z1,n__first(z0,activate(z2))) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0)),n__terms(s(z0))) terms(z0) -> n__terms(z0) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE,ADD,DBL,FIRST,SQR,TERMS,activate,add,dbl,first ,sqr,terms} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first,n__terms,nil ,recip,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: ACTIVATE(z0) -> c14() ACTIVATE(n__first(z0,z1)) -> c13(FIRST(z0,z1)) ACTIVATE(n__terms(z0)) -> c12(TERMS(z0)) ADD(0(),z0) -> c7() ADD(s(z0),z1) -> c8(ADD(z0,z1)) DBL(0()) -> c5() DBL(s(z0)) -> c6(DBL(z0)) FIRST(z0,z1) -> c11() FIRST(0(),z0) -> c9() FIRST(s(z0),cons(z1,z2)) -> c10(ACTIVATE(z2)) SQR(0()) -> c2() SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c4(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(SQR(z0)) TERMS(z0) -> c1() - Weak TRS: activate(z0) -> z0 activate(n__first(z0,z1)) -> first(z0,z1) activate(n__terms(z0)) -> terms(z0) add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) first(z0,z1) -> n__first(z0,z1) first(0(),z0) -> nil() first(s(z0),cons(z1,z2)) -> cons(z1,n__first(z0,activate(z2))) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0)),n__terms(s(z0))) terms(z0) -> n__terms(z0) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE,ADD,DBL,FIRST,SQR,TERMS,activate,add,dbl,first ,sqr,terms} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first,n__terms,nil ,recip,s} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: ADD(x,y){x -> s(x)} = ADD(s(x),y) ->^+ c8(ADD(x,y)) = C[ADD(x,y) = ADD(x,y){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: ACTIVATE(z0) -> c14() ACTIVATE(n__first(z0,z1)) -> c13(FIRST(z0,z1)) ACTIVATE(n__terms(z0)) -> c12(TERMS(z0)) ADD(0(),z0) -> c7() ADD(s(z0),z1) -> c8(ADD(z0,z1)) DBL(0()) -> c5() DBL(s(z0)) -> c6(DBL(z0)) FIRST(z0,z1) -> c11() FIRST(0(),z0) -> c9() FIRST(s(z0),cons(z1,z2)) -> c10(ACTIVATE(z2)) SQR(0()) -> c2() SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c4(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(SQR(z0)) TERMS(z0) -> c1() - Weak TRS: activate(z0) -> z0 activate(n__first(z0,z1)) -> first(z0,z1) activate(n__terms(z0)) -> terms(z0) add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) first(z0,z1) -> n__first(z0,z1) first(0(),z0) -> nil() first(s(z0),cons(z1,z2)) -> cons(z1,n__first(z0,activate(z2))) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0)),n__terms(s(z0))) terms(z0) -> n__terms(z0) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE,ADD,DBL,FIRST,SQR,TERMS,activate,add,dbl,first ,sqr,terms} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first,n__terms,nil ,recip,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs ACTIVATE#(z0) -> c_1() ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) ADD#(0(),z0) -> c_4() ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)) DBL#(0()) -> c_6() DBL#(s(z0)) -> c_7(DBL#(z0)) FIRST#(z0,z1) -> c_8() FIRST#(0(),z0) -> c_9() FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) SQR#(0()) -> c_11() SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)) SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)) TERMS#(z0) -> c_14(SQR#(z0)) TERMS#(z0) -> c_15() Weak DPs activate#(z0) -> c_16() activate#(n__first(z0,z1)) -> c_17(first#(z0,z1)) activate#(n__terms(z0)) -> c_18(terms#(z0)) add#(0(),z0) -> c_19() add#(s(z0),z1) -> c_20(add#(z0,z1)) dbl#(0()) -> c_21() dbl#(s(z0)) -> c_22(dbl#(z0)) first#(z0,z1) -> c_23() first#(0(),z0) -> c_24() first#(s(z0),cons(z1,z2)) -> c_25(activate#(z2)) sqr#(0()) -> c_26() sqr#(s(z0)) -> c_27(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)) terms#(z0) -> c_28(sqr#(z0)) terms#(z0) -> c_29() and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: ACTIVATE#(z0) -> c_1() ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) ADD#(0(),z0) -> c_4() ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)) DBL#(0()) -> c_6() DBL#(s(z0)) -> c_7(DBL#(z0)) FIRST#(z0,z1) -> c_8() FIRST#(0(),z0) -> c_9() FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) SQR#(0()) -> c_11() SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)) SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)) TERMS#(z0) -> c_14(SQR#(z0)) TERMS#(z0) -> c_15() - Weak DPs: activate#(z0) -> c_16() activate#(n__first(z0,z1)) -> c_17(first#(z0,z1)) activate#(n__terms(z0)) -> c_18(terms#(z0)) add#(0(),z0) -> c_19() add#(s(z0),z1) -> c_20(add#(z0,z1)) dbl#(0()) -> c_21() dbl#(s(z0)) -> c_22(dbl#(z0)) first#(z0,z1) -> c_23() first#(0(),z0) -> c_24() first#(s(z0),cons(z1,z2)) -> c_25(activate#(z2)) sqr#(0()) -> c_26() sqr#(s(z0)) -> c_27(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)) terms#(z0) -> c_28(sqr#(z0)) terms#(z0) -> c_29() - Weak TRS: ACTIVATE(z0) -> c14() ACTIVATE(n__first(z0,z1)) -> c13(FIRST(z0,z1)) ACTIVATE(n__terms(z0)) -> c12(TERMS(z0)) ADD(0(),z0) -> c7() ADD(s(z0),z1) -> c8(ADD(z0,z1)) DBL(0()) -> c5() DBL(s(z0)) -> c6(DBL(z0)) FIRST(z0,z1) -> c11() FIRST(0(),z0) -> c9() FIRST(s(z0),cons(z1,z2)) -> c10(ACTIVATE(z2)) SQR(0()) -> c2() SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c4(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(SQR(z0)) TERMS(z0) -> c1() activate(z0) -> z0 activate(n__first(z0,z1)) -> first(z0,z1) activate(n__terms(z0)) -> terms(z0) add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) first(z0,z1) -> n__first(z0,z1) first(0(),z0) -> nil() first(s(z0),cons(z1,z2)) -> cons(z1,n__first(z0,activate(z2))) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0)),n__terms(s(z0))) terms(z0) -> n__terms(z0) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1,ACTIVATE#/1 ,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1,activate#/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/4,c_13/4,c_14/1,c_15/0 ,c_16/0,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/3,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add# ,dbl#,first#,sqr#,terms#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first ,n__terms,nil,recip,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,4,6,8,9,11,15} by application of Pre({1,4,6,8,9,11,15}) = {2,3,5,7,10,12,13,14}. Here rules are labelled as follows: 1: ACTIVATE#(z0) -> c_1() 2: ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) 3: ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) 4: ADD#(0(),z0) -> c_4() 5: ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)) 6: DBL#(0()) -> c_6() 7: DBL#(s(z0)) -> c_7(DBL#(z0)) 8: FIRST#(z0,z1) -> c_8() 9: FIRST#(0(),z0) -> c_9() 10: FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) 11: SQR#(0()) -> c_11() 12: SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)) 13: SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)) 14: TERMS#(z0) -> c_14(SQR#(z0)) 15: TERMS#(z0) -> c_15() 16: activate#(z0) -> c_16() 17: activate#(n__first(z0,z1)) -> c_17(first#(z0,z1)) 18: activate#(n__terms(z0)) -> c_18(terms#(z0)) 19: add#(0(),z0) -> c_19() 20: add#(s(z0),z1) -> c_20(add#(z0,z1)) 21: dbl#(0()) -> c_21() 22: dbl#(s(z0)) -> c_22(dbl#(z0)) 23: first#(z0,z1) -> c_23() 24: first#(0(),z0) -> c_24() 25: first#(s(z0),cons(z1,z2)) -> c_25(activate#(z2)) 26: sqr#(0()) -> c_26() 27: sqr#(s(z0)) -> c_27(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)) 28: terms#(z0) -> c_28(sqr#(z0)) 29: terms#(z0) -> c_29() ** Step 1.b:3: RemoveWeakSuffixes. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)) DBL#(s(z0)) -> c_7(DBL#(z0)) FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)) SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)) TERMS#(z0) -> c_14(SQR#(z0)) - Weak DPs: ACTIVATE#(z0) -> c_1() ADD#(0(),z0) -> c_4() DBL#(0()) -> c_6() FIRST#(z0,z1) -> c_8() FIRST#(0(),z0) -> c_9() SQR#(0()) -> c_11() TERMS#(z0) -> c_15() activate#(z0) -> c_16() activate#(n__first(z0,z1)) -> c_17(first#(z0,z1)) activate#(n__terms(z0)) -> c_18(terms#(z0)) add#(0(),z0) -> c_19() add#(s(z0),z1) -> c_20(add#(z0,z1)) dbl#(0()) -> c_21() dbl#(s(z0)) -> c_22(dbl#(z0)) first#(z0,z1) -> c_23() first#(0(),z0) -> c_24() first#(s(z0),cons(z1,z2)) -> c_25(activate#(z2)) sqr#(0()) -> c_26() sqr#(s(z0)) -> c_27(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)) terms#(z0) -> c_28(sqr#(z0)) terms#(z0) -> c_29() - Weak TRS: ACTIVATE(z0) -> c14() ACTIVATE(n__first(z0,z1)) -> c13(FIRST(z0,z1)) ACTIVATE(n__terms(z0)) -> c12(TERMS(z0)) ADD(0(),z0) -> c7() ADD(s(z0),z1) -> c8(ADD(z0,z1)) DBL(0()) -> c5() DBL(s(z0)) -> c6(DBL(z0)) FIRST(z0,z1) -> c11() FIRST(0(),z0) -> c9() FIRST(s(z0),cons(z1,z2)) -> c10(ACTIVATE(z2)) SQR(0()) -> c2() SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c4(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(SQR(z0)) TERMS(z0) -> c1() activate(z0) -> z0 activate(n__first(z0,z1)) -> first(z0,z1) activate(n__terms(z0)) -> terms(z0) add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) first(z0,z1) -> n__first(z0,z1) first(0(),z0) -> nil() first(s(z0),cons(z1,z2)) -> cons(z1,n__first(z0,activate(z2))) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0)),n__terms(s(z0))) terms(z0) -> n__terms(z0) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1,ACTIVATE#/1 ,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1,activate#/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/4,c_13/4,c_14/1,c_15/0 ,c_16/0,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/3,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add# ,dbl#,first#,sqr#,terms#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first ,n__terms,nil,recip,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) -->_1 FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)):5 -->_1 FIRST#(0(),z0) -> c_9():13 -->_1 FIRST#(z0,z1) -> c_8():12 2:S:ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) -->_1 TERMS#(z0) -> c_14(SQR#(z0)):8 -->_1 TERMS#(z0) -> c_15():15 3:S:ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)) -->_1 ADD#(0(),z0) -> c_4():10 -->_1 ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)):3 4:S:DBL#(s(z0)) -> c_7(DBL#(z0)) -->_1 DBL#(0()) -> c_6():11 -->_1 DBL#(s(z0)) -> c_7(DBL#(z0)):4 5:S:FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) -->_1 ACTIVATE#(z0) -> c_1():9 -->_1 ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)):2 -->_1 ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)):1 6:S:SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)) -->_2 sqr#(s(z0)) -> c_27(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)):27 -->_3 dbl#(s(z0)) -> c_22(dbl#(z0)):22 -->_4 SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)):7 -->_2 sqr#(0()) -> c_26():26 -->_3 dbl#(0()) -> c_21():21 -->_4 SQR#(0()) -> c_11():14 -->_1 ADD#(0(),z0) -> c_4():10 -->_4 SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)):6 -->_1 ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)):3 7:S:SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)) -->_2 sqr#(s(z0)) -> c_27(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)):27 -->_3 dbl#(s(z0)) -> c_22(dbl#(z0)):22 -->_2 sqr#(0()) -> c_26():26 -->_3 dbl#(0()) -> c_21():21 -->_4 DBL#(0()) -> c_6():11 -->_1 ADD#(0(),z0) -> c_4():10 -->_4 DBL#(s(z0)) -> c_7(DBL#(z0)):4 -->_1 ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)):3 8:S:TERMS#(z0) -> c_14(SQR#(z0)) -->_1 SQR#(0()) -> c_11():14 -->_1 SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)):7 -->_1 SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)):6 9:W:ACTIVATE#(z0) -> c_1() 10:W:ADD#(0(),z0) -> c_4() 11:W:DBL#(0()) -> c_6() 12:W:FIRST#(z0,z1) -> c_8() 13:W:FIRST#(0(),z0) -> c_9() 14:W:SQR#(0()) -> c_11() 15:W:TERMS#(z0) -> c_15() 16:W:activate#(z0) -> c_16() 17:W:activate#(n__first(z0,z1)) -> c_17(first#(z0,z1)) -->_1 first#(s(z0),cons(z1,z2)) -> c_25(activate#(z2)):25 -->_1 first#(0(),z0) -> c_24():24 -->_1 first#(z0,z1) -> c_23():23 18:W:activate#(n__terms(z0)) -> c_18(terms#(z0)) -->_1 terms#(z0) -> c_28(sqr#(z0)):28 -->_1 terms#(z0) -> c_29():29 19:W:add#(0(),z0) -> c_19() 20:W:add#(s(z0),z1) -> c_20(add#(z0,z1)) -->_1 add#(s(z0),z1) -> c_20(add#(z0,z1)):20 -->_1 add#(0(),z0) -> c_19():19 21:W:dbl#(0()) -> c_21() 22:W:dbl#(s(z0)) -> c_22(dbl#(z0)) -->_1 dbl#(s(z0)) -> c_22(dbl#(z0)):22 -->_1 dbl#(0()) -> c_21():21 23:W:first#(z0,z1) -> c_23() 24:W:first#(0(),z0) -> c_24() 25:W:first#(s(z0),cons(z1,z2)) -> c_25(activate#(z2)) -->_1 activate#(n__terms(z0)) -> c_18(terms#(z0)):18 -->_1 activate#(n__first(z0,z1)) -> c_17(first#(z0,z1)):17 -->_1 activate#(z0) -> c_16():16 26:W:sqr#(0()) -> c_26() 27:W:sqr#(s(z0)) -> c_27(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)) -->_2 sqr#(s(z0)) -> c_27(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)):27 -->_2 sqr#(0()) -> c_26():26 -->_3 dbl#(s(z0)) -> c_22(dbl#(z0)):22 -->_3 dbl#(0()) -> c_21():21 -->_1 add#(s(z0),z1) -> c_20(add#(z0,z1)):20 -->_1 add#(0(),z0) -> c_19():19 28:W:terms#(z0) -> c_28(sqr#(z0)) -->_1 sqr#(s(z0)) -> c_27(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)):27 -->_1 sqr#(0()) -> c_26():26 29:W:terms#(z0) -> c_29() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 17: activate#(n__first(z0,z1)) -> c_17(first#(z0,z1)) 25: first#(s(z0),cons(z1,z2)) -> c_25(activate#(z2)) 23: first#(z0,z1) -> c_23() 24: first#(0(),z0) -> c_24() 18: activate#(n__terms(z0)) -> c_18(terms#(z0)) 29: terms#(z0) -> c_29() 28: terms#(z0) -> c_28(sqr#(z0)) 16: activate#(z0) -> c_16() 12: FIRST#(z0,z1) -> c_8() 13: FIRST#(0(),z0) -> c_9() 15: TERMS#(z0) -> c_15() 10: ADD#(0(),z0) -> c_4() 11: DBL#(0()) -> c_6() 27: sqr#(s(z0)) -> c_27(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)) 20: add#(s(z0),z1) -> c_20(add#(z0,z1)) 19: add#(0(),z0) -> c_19() 22: dbl#(s(z0)) -> c_22(dbl#(z0)) 21: dbl#(0()) -> c_21() 26: sqr#(0()) -> c_26() 14: SQR#(0()) -> c_11() 9: ACTIVATE#(z0) -> c_1() ** Step 1.b:4: SimplifyRHS. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)) DBL#(s(z0)) -> c_7(DBL#(z0)) FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)) SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)) TERMS#(z0) -> c_14(SQR#(z0)) - Weak TRS: ACTIVATE(z0) -> c14() ACTIVATE(n__first(z0,z1)) -> c13(FIRST(z0,z1)) ACTIVATE(n__terms(z0)) -> c12(TERMS(z0)) ADD(0(),z0) -> c7() ADD(s(z0),z1) -> c8(ADD(z0,z1)) DBL(0()) -> c5() DBL(s(z0)) -> c6(DBL(z0)) FIRST(z0,z1) -> c11() FIRST(0(),z0) -> c9() FIRST(s(z0),cons(z1,z2)) -> c10(ACTIVATE(z2)) SQR(0()) -> c2() SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c4(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(SQR(z0)) TERMS(z0) -> c1() activate(z0) -> z0 activate(n__first(z0,z1)) -> first(z0,z1) activate(n__terms(z0)) -> terms(z0) add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) first(z0,z1) -> n__first(z0,z1) first(0(),z0) -> nil() first(s(z0),cons(z1,z2)) -> cons(z1,n__first(z0,activate(z2))) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0)),n__terms(s(z0))) terms(z0) -> n__terms(z0) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1,ACTIVATE#/1 ,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1,activate#/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/4,c_13/4,c_14/1,c_15/0 ,c_16/0,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/3,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add# ,dbl#,first#,sqr#,terms#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first ,n__terms,nil,recip,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) -->_1 FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)):5 2:S:ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) -->_1 TERMS#(z0) -> c_14(SQR#(z0)):8 3:S:ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)) -->_1 ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)):3 4:S:DBL#(s(z0)) -> c_7(DBL#(z0)) -->_1 DBL#(s(z0)) -> c_7(DBL#(z0)):4 5:S:FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) -->_1 ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)):2 -->_1 ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)):1 6:S:SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)) -->_4 SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)):7 -->_4 SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)):6 -->_1 ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)):3 7:S:SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)) -->_4 DBL#(s(z0)) -> c_7(DBL#(z0)):4 -->_1 ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)):3 8:S:TERMS#(z0) -> c_14(SQR#(z0)) -->_1 SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)):7 -->_1 SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)):6 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),SQR#(z0)) SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) ** Step 1.b:5: UsableRules. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)) DBL#(s(z0)) -> c_7(DBL#(z0)) FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),SQR#(z0)) SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) TERMS#(z0) -> c_14(SQR#(z0)) - Weak TRS: ACTIVATE(z0) -> c14() ACTIVATE(n__first(z0,z1)) -> c13(FIRST(z0,z1)) ACTIVATE(n__terms(z0)) -> c12(TERMS(z0)) ADD(0(),z0) -> c7() ADD(s(z0),z1) -> c8(ADD(z0,z1)) DBL(0()) -> c5() DBL(s(z0)) -> c6(DBL(z0)) FIRST(z0,z1) -> c11() FIRST(0(),z0) -> c9() FIRST(s(z0),cons(z1,z2)) -> c10(ACTIVATE(z2)) SQR(0()) -> c2() SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c4(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(SQR(z0)) TERMS(z0) -> c1() activate(z0) -> z0 activate(n__first(z0,z1)) -> first(z0,z1) activate(n__terms(z0)) -> terms(z0) add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) first(z0,z1) -> n__first(z0,z1) first(0(),z0) -> nil() first(s(z0),cons(z1,z2)) -> cons(z1,n__first(z0,activate(z2))) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0)),n__terms(s(z0))) terms(z0) -> n__terms(z0) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1,ACTIVATE#/1 ,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1,activate#/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/0 ,c_16/0,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/3,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add# ,dbl#,first#,sqr#,terms#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first ,n__terms,nil,recip,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)) DBL#(s(z0)) -> c_7(DBL#(z0)) FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),SQR#(z0)) SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) TERMS#(z0) -> c_14(SQR#(z0)) ** Step 1.b:6: DecomposeDG. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)) DBL#(s(z0)) -> c_7(DBL#(z0)) FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),SQR#(z0)) SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) TERMS#(z0) -> c_14(SQR#(z0)) - Weak TRS: add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1,ACTIVATE#/1 ,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1,activate#/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/0 ,c_16/0,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/3,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add# ,dbl#,first#,sqr#,terms#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first ,n__terms,nil,recip,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),SQR#(z0)) TERMS#(z0) -> c_14(SQR#(z0)) and a lower component ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)) DBL#(s(z0)) -> c_7(DBL#(z0)) SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) Further, following extension rules are added to the lower component. ACTIVATE#(n__first(z0,z1)) -> FIRST#(z0,z1) ACTIVATE#(n__terms(z0)) -> TERMS#(z0) FIRST#(s(z0),cons(z1,z2)) -> ACTIVATE#(z2) SQR#(s(z0)) -> ADD#(sqr(z0),dbl(z0)) SQR#(s(z0)) -> SQR#(z0) TERMS#(z0) -> SQR#(z0) *** Step 1.b:6.a:1: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),SQR#(z0)) TERMS#(z0) -> c_14(SQR#(z0)) - Weak TRS: add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1,ACTIVATE#/1 ,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1,activate#/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/0 ,c_16/0,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/3,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add# ,dbl#,first#,sqr#,terms#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first ,n__terms,nil,recip,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) -->_1 FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)):3 2:S:ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) -->_1 TERMS#(z0) -> c_14(SQR#(z0)):5 3:S:FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) -->_1 ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)):2 -->_1 ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)):1 4:S:SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),SQR#(z0)) -->_2 SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),SQR#(z0)):4 5:S:TERMS#(z0) -> c_14(SQR#(z0)) -->_1 SQR#(s(z0)) -> c_12(ADD#(sqr(z0),dbl(z0)),SQR#(z0)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: SQR#(s(z0)) -> c_12(SQR#(z0)) *** Step 1.b:6.a:2: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) SQR#(s(z0)) -> c_12(SQR#(z0)) TERMS#(z0) -> c_14(SQR#(z0)) - Weak TRS: add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1,ACTIVATE#/1 ,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1,activate#/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2,c_14/1,c_15/0 ,c_16/0,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/3,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add# ,dbl#,first#,sqr#,terms#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first ,n__terms,nil,recip,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) SQR#(s(z0)) -> c_12(SQR#(z0)) TERMS#(z0) -> c_14(SQR#(z0)) *** Step 1.b:6.a:3: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) SQR#(s(z0)) -> c_12(SQR#(z0)) TERMS#(z0) -> c_14(SQR#(z0)) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1,ACTIVATE#/1 ,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1,activate#/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2,c_14/1,c_15/0 ,c_16/0,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/3,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add# ,dbl#,first#,sqr#,terms#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first ,n__terms,nil,recip,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any 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_3) = {1}, uargs(c_10) = {1}, uargs(c_12) = {1}, uargs(c_14) = {1} Following symbols are considered usable: {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add#,dbl#,first#,sqr#,terms#} TcT has computed the following interpretation: p(0) = [0] p(ACTIVATE) = [1] x1 + [0] p(ADD) = [2] p(DBL) = [2] x1 + [0] p(FIRST) = [2] p(SQR) = [1] p(TERMS) = [0] p(activate) = [0] p(add) = [1] x1 + [4] x2 + [1] p(c) = [1] p(c1) = [4] p(c10) = [2] p(c11) = [1] p(c12) = [0] p(c13) = [0] p(c14) = [0] p(c2) = [1] p(c3) = [1] x1 + [1] x2 + [1] p(c4) = [0] p(c5) = [1] p(c6) = [2] p(c7) = [0] p(c8) = [1] p(c9) = [1] p(cons) = [1] x2 + [0] p(dbl) = [1] p(first) = [2] x1 + [1] p(n__first) = [1] x1 + [1] x2 + [0] p(n__terms) = [1] x1 + [2] p(nil) = [1] p(recip) = [0] p(s) = [1] x1 + [8] p(sqr) = [0] p(terms) = [1] x1 + [0] p(ACTIVATE#) = [9] x1 + [12] p(ADD#) = [1] x1 + [1] x2 + [2] p(DBL#) = [1] x1 + [0] p(FIRST#) = [3] x1 + [9] x2 + [0] p(SQR#) = [2] x1 + [2] p(TERMS#) = [4] x1 + [11] p(activate#) = [1] x1 + [2] p(add#) = [1] x1 + [8] x2 + [4] p(dbl#) = [8] p(first#) = [2] p(sqr#) = [1] x1 + [1] p(terms#) = [4] p(c_1) = [8] p(c_2) = [1] x1 + [4] p(c_3) = [2] x1 + [7] p(c_4) = [0] p(c_5) = [1] x1 + [2] p(c_6) = [2] p(c_7) = [1] x1 + [1] p(c_8) = [0] p(c_9) = [0] p(c_10) = [1] x1 + [12] p(c_11) = [0] p(c_12) = [1] x1 + [8] p(c_13) = [2] x2 + [0] p(c_14) = [2] x1 + [7] p(c_15) = [0] p(c_16) = [1] p(c_17) = [2] x1 + [8] p(c_18) = [1] x1 + [0] p(c_19) = [0] p(c_20) = [4] x1 + [4] p(c_21) = [1] p(c_22) = [1] x1 + [1] p(c_23) = [1] p(c_24) = [2] p(c_25) = [1] p(c_26) = [1] p(c_27) = [4] x2 + [1] x3 + [2] p(c_28) = [1] x1 + [0] p(c_29) = [1] Following rules are strictly oriented: ACTIVATE#(n__first(z0,z1)) = [9] z0 + [9] z1 + [12] > [3] z0 + [9] z1 + [4] = c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) = [9] z0 + [30] > [8] z0 + [29] = c_3(TERMS#(z0)) SQR#(s(z0)) = [2] z0 + [18] > [2] z0 + [10] = c_12(SQR#(z0)) Following rules are (at-least) weakly oriented: FIRST#(s(z0),cons(z1,z2)) = [3] z0 + [9] z2 + [24] >= [9] z2 + [24] = c_10(ACTIVATE#(z2)) TERMS#(z0) = [4] z0 + [11] >= [4] z0 + [11] = c_14(SQR#(z0)) *** Step 1.b:6.a:4: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) TERMS#(z0) -> c_14(SQR#(z0)) - Weak DPs: ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) SQR#(s(z0)) -> c_12(SQR#(z0)) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1,ACTIVATE#/1 ,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1,activate#/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2,c_14/1,c_15/0 ,c_16/0,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/3,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add# ,dbl#,first#,sqr#,terms#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first ,n__terms,nil,recip,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any 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_3) = {1}, uargs(c_10) = {1}, uargs(c_12) = {1}, uargs(c_14) = {1} Following symbols are considered usable: {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add#,dbl#,first#,sqr#,terms#} TcT has computed the following interpretation: p(0) = [1] p(ACTIVATE) = [1] p(ADD) = [8] x2 + [8] p(DBL) = [1] p(FIRST) = [1] x1 + [1] x2 + [0] p(SQR) = [1] p(TERMS) = [4] x1 + [0] p(activate) = [1] p(add) = [1] x2 + [2] p(c) = [2] p(c1) = [1] p(c10) = [1] p(c11) = [0] p(c12) = [1] p(c13) = [0] p(c14) = [0] p(c2) = [1] p(c3) = [1] p(c4) = [1] p(c5) = [0] p(c6) = [0] p(c7) = [1] p(c8) = [0] p(c9) = [1] p(cons) = [1] x1 + [1] x2 + [0] p(dbl) = [2] p(first) = [8] x1 + [0] p(n__first) = [1] x2 + [2] p(n__terms) = [0] p(nil) = [0] p(recip) = [0] p(s) = [1] p(sqr) = [8] p(terms) = [1] x1 + [1] p(ACTIVATE#) = [8] x1 + [12] p(ADD#) = [1] p(DBL#) = [0] p(FIRST#) = [8] x2 + [14] p(SQR#) = [0] p(TERMS#) = [0] p(activate#) = [2] p(add#) = [1] p(dbl#) = [2] p(first#) = [1] x2 + [1] p(sqr#) = [1] p(terms#) = [2] p(c_1) = [1] p(c_2) = [1] x1 + [1] p(c_3) = [8] x1 + [12] p(c_4) = [1] p(c_5) = [1] x1 + [4] p(c_6) = [4] p(c_7) = [0] p(c_8) = [4] p(c_9) = [2] p(c_10) = [1] x1 + [0] p(c_11) = [1] p(c_12) = [8] x1 + [0] p(c_13) = [1] x2 + [1] p(c_14) = [4] x1 + [0] p(c_15) = [1] p(c_16) = [0] p(c_17) = [2] p(c_18) = [1] x1 + [1] p(c_19) = [1] p(c_20) = [2] p(c_21) = [0] p(c_22) = [1] x1 + [0] p(c_23) = [1] p(c_24) = [1] p(c_25) = [1] x1 + [1] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] Following rules are strictly oriented: FIRST#(s(z0),cons(z1,z2)) = [8] z1 + [8] z2 + [14] > [8] z2 + [12] = c_10(ACTIVATE#(z2)) Following rules are (at-least) weakly oriented: ACTIVATE#(n__first(z0,z1)) = [8] z1 + [28] >= [8] z1 + [15] = c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) = [12] >= [12] = c_3(TERMS#(z0)) SQR#(s(z0)) = [0] >= [0] = c_12(SQR#(z0)) TERMS#(z0) = [0] >= [0] = c_14(SQR#(z0)) *** Step 1.b:6.a:5: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: TERMS#(z0) -> c_14(SQR#(z0)) - Weak DPs: ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) SQR#(s(z0)) -> c_12(SQR#(z0)) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1,ACTIVATE#/1 ,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1,activate#/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2,c_14/1,c_15/0 ,c_16/0,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/3,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add# ,dbl#,first#,sqr#,terms#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first ,n__terms,nil,recip,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_3) = {1}, uargs(c_10) = {1}, uargs(c_12) = {1}, uargs(c_14) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(ACTIVATE) = [0] p(ADD) = [0] p(DBL) = [0] p(FIRST) = [0] p(SQR) = [0] p(TERMS) = [0] p(activate) = [0] p(add) = [0] p(c) = [1] x1 + [0] p(c1) = [0] p(c10) = [1] x1 + [0] p(c11) = [0] p(c12) = [1] x1 + [0] p(c13) = [1] x1 + [0] p(c14) = [0] p(c2) = [0] p(c3) = [1] x1 + [1] x2 + [0] p(c4) = [1] x1 + [1] x2 + [0] p(c5) = [0] p(c6) = [1] x1 + [0] p(c7) = [0] p(c8) = [1] x1 + [0] p(c9) = [0] p(cons) = [1] x1 + [1] x2 + [0] p(dbl) = [0] p(first) = [0] p(n__first) = [1] x1 + [1] x2 + [0] p(n__terms) = [1] p(nil) = [0] p(recip) = [1] x1 + [0] p(s) = [1] x1 + [0] p(sqr) = [0] p(terms) = [0] p(ACTIVATE#) = [1] x1 + [0] p(ADD#) = [0] p(DBL#) = [0] p(FIRST#) = [1] x2 + [0] p(SQR#) = [0] p(TERMS#) = [1] p(activate#) = [0] p(add#) = [0] p(dbl#) = [0] p(first#) = [0] p(sqr#) = [0] p(terms#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [1] x1 + [0] p(c_11) = [0] p(c_12) = [1] x1 + [0] p(c_13) = [0] p(c_14) = [1] x1 + [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] Following rules are strictly oriented: TERMS#(z0) = [1] > [0] = c_14(SQR#(z0)) Following rules are (at-least) weakly oriented: ACTIVATE#(n__first(z0,z1)) = [1] z0 + [1] z1 + [0] >= [1] z1 + [0] = c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) = [1] >= [1] = c_3(TERMS#(z0)) FIRST#(s(z0),cons(z1,z2)) = [1] z1 + [1] z2 + [0] >= [1] z2 + [0] = c_10(ACTIVATE#(z2)) SQR#(s(z0)) = [0] >= [0] = c_12(SQR#(z0)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 1.b:6.a:6: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: ACTIVATE#(n__first(z0,z1)) -> c_2(FIRST#(z0,z1)) ACTIVATE#(n__terms(z0)) -> c_3(TERMS#(z0)) FIRST#(s(z0),cons(z1,z2)) -> c_10(ACTIVATE#(z2)) SQR#(s(z0)) -> c_12(SQR#(z0)) TERMS#(z0) -> c_14(SQR#(z0)) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1,ACTIVATE#/1 ,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1,activate#/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2,c_14/1,c_15/0 ,c_16/0,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/3,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add# ,dbl#,first#,sqr#,terms#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first ,n__terms,nil,recip,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 1.b:6.b:1: NaturalMI. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)) DBL#(s(z0)) -> c_7(DBL#(z0)) SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) - Weak DPs: ACTIVATE#(n__first(z0,z1)) -> FIRST#(z0,z1) ACTIVATE#(n__terms(z0)) -> TERMS#(z0) FIRST#(s(z0),cons(z1,z2)) -> ACTIVATE#(z2) SQR#(s(z0)) -> ADD#(sqr(z0),dbl(z0)) SQR#(s(z0)) -> SQR#(z0) TERMS#(z0) -> SQR#(z0) - Weak TRS: add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1,ACTIVATE#/1 ,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1,activate#/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/0 ,c_16/0,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/3,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add# ,dbl#,first#,sqr#,terms#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first ,n__terms,nil,recip,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_13) = {1,2} Following symbols are considered usable: {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add#,dbl#,first#,sqr#,terms#} TcT has computed the following interpretation: p(0) = [0] p(ACTIVATE) = [0] p(ADD) = [0] p(DBL) = [0] p(FIRST) = [0] p(SQR) = [0] p(TERMS) = [0] p(activate) = [0] p(add) = [8] x1 + [0] p(c) = [1] x1 + [0] p(c1) = [0] p(c10) = [1] x1 + [0] p(c11) = [0] p(c12) = [1] x1 + [0] p(c13) = [0] p(c14) = [4] p(c2) = [1] p(c3) = [0] p(c4) = [8] p(c5) = [4] p(c6) = [4] p(c7) = [1] p(c8) = [0] p(c9) = [8] p(cons) = [1] x2 + [0] p(dbl) = [0] p(first) = [1] x2 + [2] p(n__first) = [1] p(n__terms) = [1] x1 + [1] p(nil) = [1] p(recip) = [0] p(s) = [1] p(sqr) = [0] p(terms) = [1] p(ACTIVATE#) = [15] p(ADD#) = [0] p(DBL#) = [2] p(FIRST#) = [15] p(SQR#) = [14] p(TERMS#) = [15] p(activate#) = [0] p(add#) = [1] p(dbl#) = [1] x1 + [1] p(first#) = [8] x1 + [1] p(sqr#) = [1] p(terms#) = [1] x1 + [0] p(c_1) = [1] p(c_2) = [1] x1 + [2] p(c_3) = [1] x1 + [1] p(c_4) = [2] p(c_5) = [1] x1 + [0] p(c_6) = [1] p(c_7) = [1] x1 + [0] p(c_8) = [1] p(c_9) = [2] p(c_10) = [1] x1 + [1] p(c_11) = [1] p(c_12) = [1] x1 + [2] x2 + [1] p(c_13) = [4] x1 + [4] x2 + [2] p(c_14) = [1] x1 + [0] p(c_15) = [1] p(c_16) = [0] p(c_17) = [1] p(c_18) = [0] p(c_19) = [1] p(c_20) = [1] x1 + [1] p(c_21) = [1] p(c_22) = [1] x1 + [1] p(c_23) = [1] p(c_24) = [2] p(c_25) = [1] p(c_26) = [1] p(c_27) = [1] x1 + [1] x2 + [0] p(c_28) = [1] p(c_29) = [2] Following rules are strictly oriented: SQR#(s(z0)) = [14] > [10] = c_13(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) Following rules are (at-least) weakly oriented: ACTIVATE#(n__first(z0,z1)) = [15] >= [15] = FIRST#(z0,z1) ACTIVATE#(n__terms(z0)) = [15] >= [15] = TERMS#(z0) ADD#(s(z0),z1) = [0] >= [0] = c_5(ADD#(z0,z1)) DBL#(s(z0)) = [2] >= [2] = c_7(DBL#(z0)) FIRST#(s(z0),cons(z1,z2)) = [15] >= [15] = ACTIVATE#(z2) SQR#(s(z0)) = [14] >= [0] = ADD#(sqr(z0),dbl(z0)) SQR#(s(z0)) = [14] >= [14] = SQR#(z0) TERMS#(z0) = [15] >= [14] = SQR#(z0) *** Step 1.b:6.b:2: NaturalMI. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)) DBL#(s(z0)) -> c_7(DBL#(z0)) - Weak DPs: ACTIVATE#(n__first(z0,z1)) -> FIRST#(z0,z1) ACTIVATE#(n__terms(z0)) -> TERMS#(z0) FIRST#(s(z0),cons(z1,z2)) -> ACTIVATE#(z2) SQR#(s(z0)) -> ADD#(sqr(z0),dbl(z0)) SQR#(s(z0)) -> SQR#(z0) SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) TERMS#(z0) -> SQR#(z0) - Weak TRS: add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1,ACTIVATE#/1 ,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1,activate#/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/0 ,c_16/0,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/3,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add# ,dbl#,first#,sqr#,terms#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first ,n__terms,nil,recip,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_13) = {1,2} Following symbols are considered usable: {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add#,dbl#,first#,sqr#,terms#} TcT has computed the following interpretation: p(0) = [0] p(ACTIVATE) = [8] x1 + [0] p(ADD) = [1] x1 + [1] x2 + [0] p(DBL) = [1] p(FIRST) = [1] p(SQR) = [1] p(TERMS) = [2] p(activate) = [1] x1 + [0] p(add) = [8] x1 + [8] p(c) = [1] x1 + [1] p(c1) = [2] p(c10) = [0] p(c11) = [4] p(c12) = [0] p(c13) = [0] p(c14) = [0] p(c2) = [1] p(c3) = [1] x1 + [1] x2 + [4] p(c4) = [2] p(c5) = [1] p(c6) = [1] x1 + [1] p(c7) = [8] p(c8) = [4] p(c9) = [4] p(cons) = [1] x1 + [1] x2 + [0] p(dbl) = [8] p(first) = [1] x1 + [1] x2 + [1] p(n__first) = [1] x1 + [1] x2 + [2] p(n__terms) = [1] x1 + [1] p(nil) = [0] p(recip) = [0] p(s) = [1] x1 + [1] p(sqr) = [2] x1 + [0] p(terms) = [0] p(ACTIVATE#) = [8] x1 + [12] p(ADD#) = [0] p(DBL#) = [8] x1 + [0] p(FIRST#) = [6] x1 + [8] x2 + [10] p(SQR#) = [8] x1 + [0] p(TERMS#) = [8] x1 + [1] p(activate#) = [1] x1 + [0] p(add#) = [1] p(dbl#) = [1] x1 + [2] p(first#) = [1] x1 + [8] x2 + [1] p(sqr#) = [1] x1 + [1] p(terms#) = [1] x1 + [0] p(c_1) = [1] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [1] p(c_4) = [1] p(c_5) = [2] x1 + [0] p(c_6) = [1] p(c_7) = [1] x1 + [1] p(c_8) = [1] p(c_9) = [2] p(c_10) = [1] x1 + [2] p(c_11) = [1] p(c_12) = [1] x1 + [1] p(c_13) = [8] x1 + [1] x2 + [4] p(c_14) = [1] x1 + [1] p(c_15) = [1] p(c_16) = [2] p(c_17) = [8] x1 + [1] p(c_18) = [0] p(c_19) = [0] p(c_20) = [1] x1 + [8] p(c_21) = [0] p(c_22) = [1] x1 + [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [1] x1 + [4] p(c_26) = [0] p(c_27) = [1] x1 + [1] x2 + [1] x3 + [0] p(c_28) = [1] x1 + [0] p(c_29) = [1] Following rules are strictly oriented: DBL#(s(z0)) = [8] z0 + [8] > [8] z0 + [1] = c_7(DBL#(z0)) Following rules are (at-least) weakly oriented: ACTIVATE#(n__first(z0,z1)) = [8] z0 + [8] z1 + [28] >= [6] z0 + [8] z1 + [10] = FIRST#(z0,z1) ACTIVATE#(n__terms(z0)) = [8] z0 + [20] >= [8] z0 + [1] = TERMS#(z0) ADD#(s(z0),z1) = [0] >= [0] = c_5(ADD#(z0,z1)) FIRST#(s(z0),cons(z1,z2)) = [6] z0 + [8] z1 + [8] z2 + [16] >= [8] z2 + [12] = ACTIVATE#(z2) SQR#(s(z0)) = [8] z0 + [8] >= [0] = ADD#(sqr(z0),dbl(z0)) SQR#(s(z0)) = [8] z0 + [8] >= [8] z0 + [0] = SQR#(z0) SQR#(s(z0)) = [8] z0 + [8] >= [8] z0 + [4] = c_13(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) TERMS#(z0) = [8] z0 + [1] >= [8] z0 + [0] = SQR#(z0) *** Step 1.b:6.b:3: Ara. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)) - Weak DPs: ACTIVATE#(n__first(z0,z1)) -> FIRST#(z0,z1) ACTIVATE#(n__terms(z0)) -> TERMS#(z0) DBL#(s(z0)) -> c_7(DBL#(z0)) FIRST#(s(z0),cons(z1,z2)) -> ACTIVATE#(z2) SQR#(s(z0)) -> ADD#(sqr(z0),dbl(z0)) SQR#(s(z0)) -> SQR#(z0) SQR#(s(z0)) -> c_13(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) TERMS#(z0) -> SQR#(z0) - Weak TRS: add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) - Signature: {ACTIVATE/1,ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,activate/1,add/2,dbl/1,first/2,sqr/1,terms/1,ACTIVATE#/1 ,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1,activate#/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0 ,c10/1,c11/0,c12/1,c13/1,c14/0,c2/0,c3/2,c4/2,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,n__first/2,n__terms/1,nil/0 ,recip/1,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/0 ,c_16/0,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/1,c_23/0,c_24/0,c_25/1,c_26/0,c_27/3,c_28/1,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,ADD#,DBL#,FIRST#,SQR#,TERMS#,activate#,add# ,dbl#,first#,sqr#,terms#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__first ,n__terms,nil,recip,s} + Applied Processor: Ara {minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "0") :: [] -(0)-> "A"(5, 0) F (TrsFun "0") :: [] -(0)-> "A"(15, 0) F (TrsFun "0") :: [] -(0)-> "A"(0, 15) F (TrsFun "0") :: [] -(0)-> "A"(8, 0) F (TrsFun "0") :: [] -(0)-> "A"(8, 8) F (TrsFun "add") :: ["A"(5, 0) x "A"(5, 0)] -(0)-> "A"(5, 0) F (TrsFun "cons") :: ["A"(2, 0) x "A"(2, 15)] -(0)-> "A"(2, 15) F (TrsFun "dbl") :: ["A"(15, 0)] -(6)-> "A"(5, 0) F (TrsFun "n__first") :: ["A"(15, 0) x "A"(2, 15)] -(15)-> "A"(2, 15) F (TrsFun "n__terms") :: ["A"(15, 15)] -(0)-> "A"(2, 15) F (TrsFun "s") :: ["A"(5, 0)] -(5)-> "A"(5, 0) F (TrsFun "s") :: ["A"(15, 0)] -(15)-> "A"(15, 0) F (TrsFun "s") :: ["A"(15, 15)] -(15)-> "A"(0, 15) F (TrsFun "s") :: ["A"(0, 0)] -(0)-> "A"(0, 0) F (TrsFun "s") :: ["A"(1, 0)] -(1)-> "A"(1, 0) F (TrsFun "sqr") :: ["A"(0, 15)] -(0)-> "A"(5, 0) F (DpFun "ACTIVATE") :: ["A"(2, 15)] -(15)-> "A"(3, 7) F (DpFun "ADD") :: ["A"(5, 0) x "A"(0, 0)] -(7)-> "A"(5, 14) F (DpFun "DBL") :: ["A"(0, 0)] -(0)-> "A"(2, 0) F (DpFun "FIRST") :: ["A"(1, 0) x "A"(2, 15)] -(14)-> "A"(3, 7) F (DpFun "SQR") :: ["A"(0, 15)] -(15)-> "A"(5, 7) F (DpFun "TERMS") :: ["A"(9, 15)] -(15)-> "A"(3, 7) F (ComFun 5) :: ["A"(0, 0)] -(0)-> "A"(11, 15) F (ComFun 7) :: ["A"(0, 0)] -(0)-> "A"(7, 1) F (ComFun 13) :: ["A"(0, 7) x "A"(0, 0)] -(0)-> "A"(10, 7) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (ComFun 13)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 13)_A" :: ["A"(0, 1) x "A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 5)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 5)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 7)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 7)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"0\")_A" :: [] -(0)-> "A"(1, 0) "F (TrsFun \"0\")_A" :: [] -(0)-> "A"(0, 1) "F (TrsFun \"cons\")_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0) "F (TrsFun \"cons\")_A" :: ["A"(0, 0) x "A"(0, 1)] -(0)-> "A"(0, 1) "F (TrsFun \"n__first\")_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0) "F (TrsFun \"n__first\")_A" :: ["A"(0) x "A"(0)] -(1)-> "A"(0, 1) "F (TrsFun \"n__terms\")_A" :: ["A"(0)] -(0)-> "A"(1, 0) "F (TrsFun \"n__terms\")_A" :: ["A"(0)] -(0)-> "A"(0, 1) "F (TrsFun \"s\")_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0) "F (TrsFun \"s\")_A" :: ["A"(1, 1)] -(1)-> "A"(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: ADD#(s(z0),z1) -> c_5(ADD#(z0,z1)) 2. Weak: WORST_CASE(Omega(n^1),O(n^3))