WORST_CASE(Omega(n^1),O(n^3)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^3)) + Considered Problem: - Strict TRS: ADD(0(),z0) -> c6() ADD(s(z0),z1) -> c7(ADD(z0,z1)) DBL(0()) -> c4() DBL(s(z0)) -> c5(DBL(z0)) FIRST(0(),z0) -> c8() FIRST(s(z0),cons(z1)) -> c9() SQR(0()) -> c1() SQR(s(z0)) -> c2(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(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))) first(0(),z0) -> nil() first(s(z0),cons(z1)) -> cons(z1) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0))) - Signature: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1 ,c6/0,c7/1,c8/0,c9/0,cons/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD,DBL,FIRST,SQR,TERMS,add,dbl,first,sqr ,terms} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,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: ADD(0(),z0) -> c6() ADD(s(z0),z1) -> c7(ADD(z0,z1)) DBL(0()) -> c4() DBL(s(z0)) -> c5(DBL(z0)) FIRST(0(),z0) -> c8() FIRST(s(z0),cons(z1)) -> c9() SQR(0()) -> c1() SQR(s(z0)) -> c2(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(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))) first(0(),z0) -> nil() first(s(z0),cons(z1)) -> cons(z1) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0))) - Signature: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1 ,c6/0,c7/1,c8/0,c9/0,cons/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD,DBL,FIRST,SQR,TERMS,add,dbl,first,sqr ,terms} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,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: ADD(0(),z0) -> c6() ADD(s(z0),z1) -> c7(ADD(z0,z1)) DBL(0()) -> c4() DBL(s(z0)) -> c5(DBL(z0)) FIRST(0(),z0) -> c8() FIRST(s(z0),cons(z1)) -> c9() SQR(0()) -> c1() SQR(s(z0)) -> c2(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(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))) first(0(),z0) -> nil() first(s(z0),cons(z1)) -> cons(z1) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0))) - Signature: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1 ,c6/0,c7/1,c8/0,c9/0,cons/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD,DBL,FIRST,SQR,TERMS,add,dbl,first,sqr ,terms} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,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) ->^+ c7(ADD(x,y)) = C[ADD(x,y) = ADD(x,y){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: ADD(0(),z0) -> c6() ADD(s(z0),z1) -> c7(ADD(z0,z1)) DBL(0()) -> c4() DBL(s(z0)) -> c5(DBL(z0)) FIRST(0(),z0) -> c8() FIRST(s(z0),cons(z1)) -> c9() SQR(0()) -> c1() SQR(s(z0)) -> c2(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(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))) first(0(),z0) -> nil() first(s(z0),cons(z1)) -> cons(z1) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0))) - Signature: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1 ,c6/0,c7/1,c8/0,c9/0,cons/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD,DBL,FIRST,SQR,TERMS,add,dbl,first,sqr ,terms} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,recip,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs ADD#(0(),z0) -> c_1() ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) DBL#(0()) -> c_3() DBL#(s(z0)) -> c_4(DBL#(z0)) FIRST#(0(),z0) -> c_5() FIRST#(s(z0),cons(z1)) -> c_6() SQR#(0()) -> c_7() SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)) SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)) TERMS#(z0) -> c_10(SQR#(z0)) Weak DPs add#(0(),z0) -> c_11() add#(s(z0),z1) -> c_12(add#(z0,z1)) dbl#(0()) -> c_13() dbl#(s(z0)) -> c_14(dbl#(z0)) first#(0(),z0) -> c_15() first#(s(z0),cons(z1)) -> c_16() sqr#(0()) -> c_17() sqr#(s(z0)) -> c_18(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)) terms#(z0) -> c_19(sqr#(z0)) and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: ADD#(0(),z0) -> c_1() ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) DBL#(0()) -> c_3() DBL#(s(z0)) -> c_4(DBL#(z0)) FIRST#(0(),z0) -> c_5() FIRST#(s(z0),cons(z1)) -> c_6() SQR#(0()) -> c_7() SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)) SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)) TERMS#(z0) -> c_10(SQR#(z0)) - Weak DPs: add#(0(),z0) -> c_11() add#(s(z0),z1) -> c_12(add#(z0,z1)) dbl#(0()) -> c_13() dbl#(s(z0)) -> c_14(dbl#(z0)) first#(0(),z0) -> c_15() first#(s(z0),cons(z1)) -> c_16() sqr#(0()) -> c_17() sqr#(s(z0)) -> c_18(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)) terms#(z0) -> c_19(sqr#(z0)) - Weak TRS: ADD(0(),z0) -> c6() ADD(s(z0),z1) -> c7(ADD(z0,z1)) DBL(0()) -> c4() DBL(s(z0)) -> c5(DBL(z0)) FIRST(0(),z0) -> c8() FIRST(s(z0),cons(z1)) -> c9() SQR(0()) -> c1() SQR(s(z0)) -> c2(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(SQR(z0)) add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) first(0(),z0) -> nil() first(s(z0),cons(z1)) -> cons(z1) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0))) - Signature: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1 ,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1,c6/0,c7/1,c8/0,c9/0,cons/1 ,nil/0,recip/1,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/4,c_9/4,c_10/1,c_11/0,c_12/1,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/0,c_18/3,c_19/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr# ,terms#} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,recip,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,5,6,7} by application of Pre({1,3,5,6,7}) = {2,4,8,9,10}. Here rules are labelled as follows: 1: ADD#(0(),z0) -> c_1() 2: ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) 3: DBL#(0()) -> c_3() 4: DBL#(s(z0)) -> c_4(DBL#(z0)) 5: FIRST#(0(),z0) -> c_5() 6: FIRST#(s(z0),cons(z1)) -> c_6() 7: SQR#(0()) -> c_7() 8: SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)) 9: SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)) 10: TERMS#(z0) -> c_10(SQR#(z0)) 11: add#(0(),z0) -> c_11() 12: add#(s(z0),z1) -> c_12(add#(z0,z1)) 13: dbl#(0()) -> c_13() 14: dbl#(s(z0)) -> c_14(dbl#(z0)) 15: first#(0(),z0) -> c_15() 16: first#(s(z0),cons(z1)) -> c_16() 17: sqr#(0()) -> c_17() 18: sqr#(s(z0)) -> c_18(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)) 19: terms#(z0) -> c_19(sqr#(z0)) ** Step 1.b:3: RemoveWeakSuffixes. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) DBL#(s(z0)) -> c_4(DBL#(z0)) SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)) SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)) TERMS#(z0) -> c_10(SQR#(z0)) - Weak DPs: ADD#(0(),z0) -> c_1() DBL#(0()) -> c_3() FIRST#(0(),z0) -> c_5() FIRST#(s(z0),cons(z1)) -> c_6() SQR#(0()) -> c_7() add#(0(),z0) -> c_11() add#(s(z0),z1) -> c_12(add#(z0,z1)) dbl#(0()) -> c_13() dbl#(s(z0)) -> c_14(dbl#(z0)) first#(0(),z0) -> c_15() first#(s(z0),cons(z1)) -> c_16() sqr#(0()) -> c_17() sqr#(s(z0)) -> c_18(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)) terms#(z0) -> c_19(sqr#(z0)) - Weak TRS: ADD(0(),z0) -> c6() ADD(s(z0),z1) -> c7(ADD(z0,z1)) DBL(0()) -> c4() DBL(s(z0)) -> c5(DBL(z0)) FIRST(0(),z0) -> c8() FIRST(s(z0),cons(z1)) -> c9() SQR(0()) -> c1() SQR(s(z0)) -> c2(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(SQR(z0)) add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) first(0(),z0) -> nil() first(s(z0),cons(z1)) -> cons(z1) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0))) - Signature: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1 ,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1,c6/0,c7/1,c8/0,c9/0,cons/1 ,nil/0,recip/1,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/4,c_9/4,c_10/1,c_11/0,c_12/1,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/0,c_18/3,c_19/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr# ,terms#} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,recip,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) -->_1 ADD#(0(),z0) -> c_1():6 -->_1 ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)):1 2:S:DBL#(s(z0)) -> c_4(DBL#(z0)) -->_1 DBL#(0()) -> c_3():7 -->_1 DBL#(s(z0)) -> c_4(DBL#(z0)):2 3:S:SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)) -->_2 sqr#(s(z0)) -> c_18(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)):18 -->_3 dbl#(s(z0)) -> c_14(dbl#(z0)):14 -->_4 SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)):4 -->_2 sqr#(0()) -> c_17():17 -->_3 dbl#(0()) -> c_13():13 -->_4 SQR#(0()) -> c_7():10 -->_1 ADD#(0(),z0) -> c_1():6 -->_4 SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)):3 -->_1 ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)):1 4:S:SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)) -->_2 sqr#(s(z0)) -> c_18(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)):18 -->_3 dbl#(s(z0)) -> c_14(dbl#(z0)):14 -->_2 sqr#(0()) -> c_17():17 -->_3 dbl#(0()) -> c_13():13 -->_4 DBL#(0()) -> c_3():7 -->_1 ADD#(0(),z0) -> c_1():6 -->_4 DBL#(s(z0)) -> c_4(DBL#(z0)):2 -->_1 ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)):1 5:S:TERMS#(z0) -> c_10(SQR#(z0)) -->_1 SQR#(0()) -> c_7():10 -->_1 SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)):4 -->_1 SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)):3 6:W:ADD#(0(),z0) -> c_1() 7:W:DBL#(0()) -> c_3() 8:W:FIRST#(0(),z0) -> c_5() 9:W:FIRST#(s(z0),cons(z1)) -> c_6() 10:W:SQR#(0()) -> c_7() 11:W:add#(0(),z0) -> c_11() 12:W:add#(s(z0),z1) -> c_12(add#(z0,z1)) -->_1 add#(s(z0),z1) -> c_12(add#(z0,z1)):12 -->_1 add#(0(),z0) -> c_11():11 13:W:dbl#(0()) -> c_13() 14:W:dbl#(s(z0)) -> c_14(dbl#(z0)) -->_1 dbl#(s(z0)) -> c_14(dbl#(z0)):14 -->_1 dbl#(0()) -> c_13():13 15:W:first#(0(),z0) -> c_15() 16:W:first#(s(z0),cons(z1)) -> c_16() 17:W:sqr#(0()) -> c_17() 18:W:sqr#(s(z0)) -> c_18(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)) -->_2 sqr#(s(z0)) -> c_18(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)):18 -->_2 sqr#(0()) -> c_17():17 -->_3 dbl#(s(z0)) -> c_14(dbl#(z0)):14 -->_3 dbl#(0()) -> c_13():13 -->_1 add#(s(z0),z1) -> c_12(add#(z0,z1)):12 -->_1 add#(0(),z0) -> c_11():11 19:W:terms#(z0) -> c_19(sqr#(z0)) -->_1 sqr#(s(z0)) -> c_18(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)):18 -->_1 sqr#(0()) -> c_17():17 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 19: terms#(z0) -> c_19(sqr#(z0)) 16: first#(s(z0),cons(z1)) -> c_16() 15: first#(0(),z0) -> c_15() 9: FIRST#(s(z0),cons(z1)) -> c_6() 8: FIRST#(0(),z0) -> c_5() 10: SQR#(0()) -> c_7() 18: sqr#(s(z0)) -> c_18(add#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0)) 12: add#(s(z0),z1) -> c_12(add#(z0,z1)) 11: add#(0(),z0) -> c_11() 14: dbl#(s(z0)) -> c_14(dbl#(z0)) 13: dbl#(0()) -> c_13() 17: sqr#(0()) -> c_17() 7: DBL#(0()) -> c_3() 6: ADD#(0(),z0) -> c_1() ** Step 1.b:4: SimplifyRHS. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) DBL#(s(z0)) -> c_4(DBL#(z0)) SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)) SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)) TERMS#(z0) -> c_10(SQR#(z0)) - Weak TRS: ADD(0(),z0) -> c6() ADD(s(z0),z1) -> c7(ADD(z0,z1)) DBL(0()) -> c4() DBL(s(z0)) -> c5(DBL(z0)) FIRST(0(),z0) -> c8() FIRST(s(z0),cons(z1)) -> c9() SQR(0()) -> c1() SQR(s(z0)) -> c2(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(SQR(z0)) add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) first(0(),z0) -> nil() first(s(z0),cons(z1)) -> cons(z1) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0))) - Signature: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1 ,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1,c6/0,c7/1,c8/0,c9/0,cons/1 ,nil/0,recip/1,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/4,c_9/4,c_10/1,c_11/0,c_12/1,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/0,c_18/3,c_19/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr# ,terms#} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,recip,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) -->_1 ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)):1 2:S:DBL#(s(z0)) -> c_4(DBL#(z0)) -->_1 DBL#(s(z0)) -> c_4(DBL#(z0)):2 3:S:SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)) -->_4 SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)):4 -->_4 SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)):3 -->_1 ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)):1 4:S:SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)) -->_4 DBL#(s(z0)) -> c_4(DBL#(z0)):2 -->_1 ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)):1 5:S:TERMS#(z0) -> c_10(SQR#(z0)) -->_1 SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),DBL#(z0)):4 -->_1 SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),sqr#(z0),dbl#(z0),SQR#(z0)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),SQR#(z0)) SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) ** Step 1.b:5: UsableRules. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) DBL#(s(z0)) -> c_4(DBL#(z0)) SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),SQR#(z0)) SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) TERMS#(z0) -> c_10(SQR#(z0)) - Weak TRS: ADD(0(),z0) -> c6() ADD(s(z0),z1) -> c7(ADD(z0,z1)) DBL(0()) -> c4() DBL(s(z0)) -> c5(DBL(z0)) FIRST(0(),z0) -> c8() FIRST(s(z0),cons(z1)) -> c9() SQR(0()) -> c1() SQR(s(z0)) -> c2(ADD(sqr(z0),dbl(z0)),SQR(z0)) SQR(s(z0)) -> c3(ADD(sqr(z0),dbl(z0)),DBL(z0)) TERMS(z0) -> c(SQR(z0)) add(0(),z0) -> z0 add(s(z0),z1) -> s(add(z0,z1)) dbl(0()) -> 0() dbl(s(z0)) -> s(s(dbl(z0))) first(0(),z0) -> nil() first(s(z0),cons(z1)) -> cons(z1) sqr(0()) -> 0() sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) terms(z0) -> cons(recip(sqr(z0))) - Signature: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1 ,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1,c6/0,c7/1,c8/0,c9/0,cons/1 ,nil/0,recip/1,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/2,c_9/2,c_10/1,c_11/0,c_12/1,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/0,c_18/3,c_19/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr# ,terms#} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,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))) ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) DBL#(s(z0)) -> c_4(DBL#(z0)) SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),SQR#(z0)) SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) TERMS#(z0) -> c_10(SQR#(z0)) ** Step 1.b:6: RemoveHeads. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) DBL#(s(z0)) -> c_4(DBL#(z0)) SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),SQR#(z0)) SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) TERMS#(z0) -> c_10(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: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1 ,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1,c6/0,c7/1,c8/0,c9/0,cons/1 ,nil/0,recip/1,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/2,c_9/2,c_10/1,c_11/0,c_12/1,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/0,c_18/3,c_19/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr# ,terms#} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,recip,s} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) -->_1 ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)):1 2:S:DBL#(s(z0)) -> c_4(DBL#(z0)) -->_1 DBL#(s(z0)) -> c_4(DBL#(z0)):2 3:S:SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),SQR#(z0)) -->_2 SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),DBL#(z0)):4 -->_2 SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),SQR#(z0)):3 -->_1 ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)):1 4:S:SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) -->_2 DBL#(s(z0)) -> c_4(DBL#(z0)):2 -->_1 ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)):1 5:S:TERMS#(z0) -> c_10(SQR#(z0)) -->_1 SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),DBL#(z0)):4 -->_1 SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),SQR#(z0)):3 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(5,TERMS#(z0) -> c_10(SQR#(z0)))] ** Step 1.b:7: DecomposeDG. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) DBL#(s(z0)) -> c_4(DBL#(z0)) SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),SQR#(z0)) SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),DBL#(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: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1 ,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1,c6/0,c7/1,c8/0,c9/0,cons/1 ,nil/0,recip/1,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/2,c_9/2,c_10/1,c_11/0,c_12/1,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/0,c_18/3,c_19/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr# ,terms#} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,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 SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),SQR#(z0)) and a lower component ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) DBL#(s(z0)) -> c_4(DBL#(z0)) SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) Further, following extension rules are added to the lower component. SQR#(s(z0)) -> ADD#(sqr(z0),dbl(z0)) SQR#(s(z0)) -> SQR#(z0) *** Step 1.b:7.a:1: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(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: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1 ,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1,c6/0,c7/1,c8/0,c9/0,cons/1 ,nil/0,recip/1,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/2,c_9/2,c_10/1,c_11/0,c_12/1,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/0,c_18/3,c_19/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr# ,terms#} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,recip,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),SQR#(z0)) -->_2 SQR#(s(z0)) -> c_8(ADD#(sqr(z0),dbl(z0)),SQR#(z0)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: SQR#(s(z0)) -> c_8(SQR#(z0)) *** Step 1.b:7.a:2: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: SQR#(s(z0)) -> c_8(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: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1 ,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1,c6/0,c7/1,c8/0,c9/0,cons/1 ,nil/0,recip/1,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/0,c_12/1,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/0,c_18/3,c_19/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr# ,terms#} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,recip,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: SQR#(s(z0)) -> c_8(SQR#(z0)) *** Step 1.b:7.a:3: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: SQR#(s(z0)) -> c_8(SQR#(z0)) - Signature: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1 ,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1,c6/0,c7/1,c8/0,c9/0,cons/1 ,nil/0,recip/1,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/0,c_12/1,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/0,c_18/3,c_19/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr# ,terms#} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,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_8) = {1} Following symbols are considered usable: {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr#,terms#} TcT has computed the following interpretation: p(0) = [8] p(ADD) = [1] x1 + [1] x2 + [1] p(DBL) = [4] x1 + [1] p(FIRST) = [1] x2 + [8] p(SQR) = [1] p(TERMS) = [2] x1 + [1] p(add) = [8] p(c) = [0] p(c1) = [0] p(c2) = [1] p(c3) = [1] x2 + [8] p(c4) = [1] p(c5) = [1] x1 + [1] p(c6) = [0] p(c7) = [1] x1 + [0] p(c8) = [0] p(c9) = [0] p(cons) = [1] x1 + [0] p(dbl) = [0] p(first) = [0] p(nil) = [0] p(recip) = [1] x1 + [0] p(s) = [1] x1 + [2] p(sqr) = [0] p(terms) = [0] p(ADD#) = [0] p(DBL#) = [0] p(FIRST#) = [1] x2 + [0] p(SQR#) = [8] x1 + [0] p(TERMS#) = [0] p(add#) = [0] p(dbl#) = [1] x1 + [0] p(first#) = [1] x2 + [2] p(sqr#) = [4] p(terms#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] p(c_4) = [1] x1 + [1] p(c_5) = [8] p(c_6) = [1] p(c_7) = [0] p(c_8) = [1] x1 + [8] p(c_9) = [2] x1 + [1] x2 + [1] p(c_10) = [2] p(c_11) = [4] p(c_12) = [2] x1 + [1] p(c_13) = [0] p(c_14) = [2] x1 + [0] p(c_15) = [1] p(c_16) = [1] p(c_17) = [1] p(c_18) = [1] x3 + [2] p(c_19) = [0] Following rules are strictly oriented: SQR#(s(z0)) = [8] z0 + [16] > [8] z0 + [8] = c_8(SQR#(z0)) Following rules are (at-least) weakly oriented: *** Step 1.b:7.a:4: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: SQR#(s(z0)) -> c_8(SQR#(z0)) - Signature: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1 ,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1,c6/0,c7/1,c8/0,c9/0,cons/1 ,nil/0,recip/1,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/0,c_12/1,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/0,c_18/3,c_19/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr# ,terms#} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,recip,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 1.b:7.b:1: NaturalMI. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) DBL#(s(z0)) -> c_4(DBL#(z0)) SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) - Weak DPs: SQR#(s(z0)) -> ADD#(sqr(z0),dbl(z0)) SQR#(s(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: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1 ,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1,c6/0,c7/1,c8/0,c9/0,cons/1 ,nil/0,recip/1,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/2,c_9/2,c_10/1,c_11/0,c_12/1,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/0,c_18/3,c_19/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr# ,terms#} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,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_4) = {1}, uargs(c_9) = {1,2} Following symbols are considered usable: {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr#,terms#} TcT has computed the following interpretation: p(0) = [0] p(ADD) = [0] p(DBL) = [0] p(FIRST) = [0] p(SQR) = [0] p(TERMS) = [0] p(add) = [0] p(c) = [1] x1 + [0] p(c1) = [0] p(c2) = [1] x1 + [1] x2 + [0] p(c3) = [1] x1 + [1] x2 + [0] p(c4) = [0] p(c5) = [1] x1 + [0] p(c6) = [0] p(c7) = [1] x1 + [0] p(c8) = [0] p(c9) = [0] p(cons) = [1] x1 + [0] p(dbl) = [0] p(first) = [0] p(nil) = [0] p(recip) = [1] x1 + [0] p(s) = [0] p(sqr) = [0] p(terms) = [0] p(ADD#) = [0] p(DBL#) = [0] p(FIRST#) = [0] p(SQR#) = [2] p(TERMS#) = [0] p(add#) = [1] x1 + [1] x2 + [0] p(dbl#) = [2] x1 + [0] p(first#) = [1] x2 + [0] p(sqr#) = [1] x1 + [0] p(terms#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [8] x1 + [0] p(c_3) = [0] p(c_4) = [2] x1 + [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [2] p(c_8) = [1] x2 + [2] p(c_9) = [1] x1 + [8] x2 + [0] p(c_10) = [1] x1 + [1] p(c_11) = [2] p(c_12) = [8] x1 + [2] p(c_13) = [1] p(c_14) = [1] p(c_15) = [4] p(c_16) = [0] p(c_17) = [0] p(c_18) = [1] x1 + [2] x2 + [2] x3 + [2] p(c_19) = [2] x1 + [0] Following rules are strictly oriented: SQR#(s(z0)) = [2] > [0] = c_9(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) Following rules are (at-least) weakly oriented: ADD#(s(z0),z1) = [0] >= [0] = c_2(ADD#(z0,z1)) DBL#(s(z0)) = [0] >= [0] = c_4(DBL#(z0)) SQR#(s(z0)) = [2] >= [0] = ADD#(sqr(z0),dbl(z0)) SQR#(s(z0)) = [2] >= [2] = SQR#(z0) *** Step 1.b:7.b:2: NaturalMI. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) DBL#(s(z0)) -> c_4(DBL#(z0)) - Weak DPs: SQR#(s(z0)) -> ADD#(sqr(z0),dbl(z0)) SQR#(s(z0)) -> SQR#(z0) SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),DBL#(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: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1 ,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1,c6/0,c7/1,c8/0,c9/0,cons/1 ,nil/0,recip/1,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/2,c_9/2,c_10/1,c_11/0,c_12/1,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/0,c_18/3,c_19/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr# ,terms#} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,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_4) = {1}, uargs(c_9) = {1,2} Following symbols are considered usable: {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr#,terms#} TcT has computed the following interpretation: p(0) = [6] p(ADD) = [1] p(DBL) = [0] p(FIRST) = [8] x2 + [0] p(SQR) = [0] p(TERMS) = [1] x1 + [0] p(add) = [2] x1 + [4] p(c) = [2] p(c1) = [0] p(c2) = [1] x1 + [0] p(c3) = [2] p(c4) = [1] p(c5) = [1] p(c6) = [0] p(c7) = [0] p(c8) = [2] p(c9) = [1] p(cons) = [1] x1 + [0] p(dbl) = [0] p(first) = [1] x2 + [2] p(nil) = [1] p(recip) = [1] x1 + [1] p(s) = [1] x1 + [2] p(sqr) = [4] p(terms) = [1] x1 + [0] p(ADD#) = [1] p(DBL#) = [1] x1 + [0] p(FIRST#) = [1] x1 + [4] x2 + [0] p(SQR#) = [3] x1 + [14] p(TERMS#) = [0] p(add#) = [2] x1 + [4] p(dbl#) = [0] p(first#) = [1] p(sqr#) = [0] p(terms#) = [1] x1 + [2] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [1] p(c_4) = [1] x1 + [1] p(c_5) = [0] p(c_6) = [1] p(c_7) = [0] p(c_8) = [1] x1 + [2] x2 + [1] p(c_9) = [12] x1 + [2] x2 + [8] p(c_10) = [2] p(c_11) = [2] p(c_12) = [1] x1 + [0] p(c_13) = [8] p(c_14) = [1] p(c_15) = [2] p(c_16) = [1] p(c_17) = [1] p(c_18) = [1] x2 + [1] x3 + [0] p(c_19) = [0] Following rules are strictly oriented: DBL#(s(z0)) = [1] z0 + [2] > [1] z0 + [1] = c_4(DBL#(z0)) Following rules are (at-least) weakly oriented: ADD#(s(z0),z1) = [1] >= [1] = c_2(ADD#(z0,z1)) SQR#(s(z0)) = [3] z0 + [20] >= [1] = ADD#(sqr(z0),dbl(z0)) SQR#(s(z0)) = [3] z0 + [20] >= [3] z0 + [14] = SQR#(z0) SQR#(s(z0)) = [3] z0 + [20] >= [2] z0 + [20] = c_9(ADD#(sqr(z0),dbl(z0)),DBL#(z0)) *** Step 1.b:7.b:3: Ara. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) - Weak DPs: DBL#(s(z0)) -> c_4(DBL#(z0)) SQR#(s(z0)) -> ADD#(sqr(z0),dbl(z0)) SQR#(s(z0)) -> SQR#(z0) SQR#(s(z0)) -> c_9(ADD#(sqr(z0),dbl(z0)),DBL#(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: {ADD/2,DBL/1,FIRST/2,SQR/1,TERMS/1,add/2,dbl/1,first/2,sqr/1,terms/1,ADD#/2,DBL#/1,FIRST#/2,SQR#/1,TERMS#/1 ,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/1,c6/0,c7/1,c8/0,c9/0,cons/1 ,nil/0,recip/1,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/2,c_9/2,c_10/1,c_11/0,c_12/1,c_13/0,c_14/1 ,c_15/0,c_16/0,c_17/0,c_18/3,c_19/1} - Obligation: innermost runtime complexity wrt. defined symbols {ADD#,DBL#,FIRST#,SQR#,TERMS#,add#,dbl#,first#,sqr# ,terms#} and constructors {0,c,c1,c2,c3,c4,c5,c6,c7,c8,c9,cons,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"(2, 0) F (TrsFun "0") :: [] -(0)-> "A"(4, 0) F (TrsFun "0") :: [] -(0)-> "A"(5, 4) F (TrsFun "add") :: ["A"(2, 0) x "A"(2, 0)] -(0)-> "A"(2, 0) F (TrsFun "dbl") :: ["A"(4, 0)] -(0)-> "A"(2, 0) F (TrsFun "s") :: ["A"(2, 0)] -(2)-> "A"(2, 0) F (TrsFun "s") :: ["A"(4, 0)] -(4)-> "A"(4, 0) F (TrsFun "s") :: ["A"(9, 4)] -(5)-> "A"(5, 4) F (TrsFun "s") :: ["A"(1, 0)] -(1)-> "A"(1, 0) F (TrsFun "s") :: ["A"(10, 5)] -(5)-> "A"(5, 5) F (TrsFun "sqr") :: ["A"(5, 4)] -(0)-> "A"(2, 0) F (DpFun "ADD") :: ["A"(2, 0) x "A"(0, 0)] -(0)-> "A"(1, 0) F (DpFun "DBL") :: ["A"(1, 0)] -(0)-> "A"(1, 0) F (DpFun "SQR") :: ["A"(5, 5)] -(0)-> "A"(0, 0) F (ComFun 2) :: ["A"(1, 0)] -(1)-> "A"(1, 0) F (ComFun 4) :: ["A"(1, 0)] -(1)-> "A"(1, 0) F (ComFun 9) :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 1) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: ADD#(s(z0),z1) -> c_2(ADD#(z0,z1)) 2. Weak: WORST_CASE(Omega(n^1),O(n^3))