WORST_CASE(Omega(n^1),O(n^2)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^2)) + Considered Problem: - Strict TRS: GREATERS(z0,.(z1,z2)) -> c7(GREATERS(z0,z2)) GREATERS(z0,.(z1,z2)) -> c8(GREATERS(z0,z2)) GREATERS(z0,nil()) -> c6() LOWERS(z0,.(z1,z2)) -> c4(LOWERS(z0,z2)) LOWERS(z0,.(z1,z2)) -> c5(LOWERS(z0,z2)) LOWERS(z0,nil()) -> c3() QSORT(.(z0,z1)) -> c1(QSORT(lowers(z0,z1)),LOWERS(z0,z1)) QSORT(.(z0,z1)) -> c2(QSORT(greaters(z0,z1)),GREATERS(z0,z1)) QSORT(nil()) -> c() - Weak TRS: greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() qsort(.(z0,z1)) -> ++(qsort(lowers(z0,z1)),.(z0,qsort(greaters(z0,z1)))) qsort(nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0 ,c7/1,c8/1,if/3,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS,LOWERS,QSORT,greaters,lowers ,qsort} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: GREATERS(z0,.(z1,z2)) -> c7(GREATERS(z0,z2)) GREATERS(z0,.(z1,z2)) -> c8(GREATERS(z0,z2)) GREATERS(z0,nil()) -> c6() LOWERS(z0,.(z1,z2)) -> c4(LOWERS(z0,z2)) LOWERS(z0,.(z1,z2)) -> c5(LOWERS(z0,z2)) LOWERS(z0,nil()) -> c3() QSORT(.(z0,z1)) -> c1(QSORT(lowers(z0,z1)),LOWERS(z0,z1)) QSORT(.(z0,z1)) -> c2(QSORT(greaters(z0,z1)),GREATERS(z0,z1)) QSORT(nil()) -> c() - Weak TRS: greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() qsort(.(z0,z1)) -> ++(qsort(lowers(z0,z1)),.(z0,qsort(greaters(z0,z1)))) qsort(nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0 ,c7/1,c8/1,if/3,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS,LOWERS,QSORT,greaters,lowers ,qsort} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: GREATERS(z0,.(z1,z2)) -> c7(GREATERS(z0,z2)) GREATERS(z0,.(z1,z2)) -> c8(GREATERS(z0,z2)) GREATERS(z0,nil()) -> c6() LOWERS(z0,.(z1,z2)) -> c4(LOWERS(z0,z2)) LOWERS(z0,.(z1,z2)) -> c5(LOWERS(z0,z2)) LOWERS(z0,nil()) -> c3() QSORT(.(z0,z1)) -> c1(QSORT(lowers(z0,z1)),LOWERS(z0,z1)) QSORT(.(z0,z1)) -> c2(QSORT(greaters(z0,z1)),GREATERS(z0,z1)) QSORT(nil()) -> c() - Weak TRS: greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() qsort(.(z0,z1)) -> ++(qsort(lowers(z0,z1)),.(z0,qsort(greaters(z0,z1)))) qsort(nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0 ,c7/1,c8/1,if/3,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS,LOWERS,QSORT,greaters,lowers ,qsort} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: GREATERS(x,z){z -> .(y,z)} = GREATERS(x,.(y,z)) ->^+ c7(GREATERS(x,z)) = C[GREATERS(x,z) = GREATERS(x,z){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: GREATERS(z0,.(z1,z2)) -> c7(GREATERS(z0,z2)) GREATERS(z0,.(z1,z2)) -> c8(GREATERS(z0,z2)) GREATERS(z0,nil()) -> c6() LOWERS(z0,.(z1,z2)) -> c4(LOWERS(z0,z2)) LOWERS(z0,.(z1,z2)) -> c5(LOWERS(z0,z2)) LOWERS(z0,nil()) -> c3() QSORT(.(z0,z1)) -> c1(QSORT(lowers(z0,z1)),LOWERS(z0,z1)) QSORT(.(z0,z1)) -> c2(QSORT(greaters(z0,z1)),GREATERS(z0,z1)) QSORT(nil()) -> c() - Weak TRS: greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() qsort(.(z0,z1)) -> ++(qsort(lowers(z0,z1)),.(z0,qsort(greaters(z0,z1)))) qsort(nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0 ,c7/1,c8/1,if/3,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS,LOWERS,QSORT,greaters,lowers ,qsort} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) GREATERS#(z0,nil()) -> c_3() LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) LOWERS#(z0,nil()) -> c_6() QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),lowers#(z0,z1),LOWERS#(z0,z1)) QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),greaters#(z0,z1),GREATERS#(z0,z1)) QSORT#(nil()) -> c_9() Weak DPs greaters#(z0,.(z1,z2)) -> c_10(greaters#(z0,z2),greaters#(z0,z2)) greaters#(z0,nil()) -> c_11() lowers#(z0,.(z1,z2)) -> c_12(lowers#(z0,z2),lowers#(z0,z2)) lowers#(z0,nil()) -> c_13() qsort#(.(z0,z1)) -> c_14(qsort#(lowers(z0,z1)),lowers#(z0,z1),qsort#(greaters(z0,z1)),greaters#(z0,z1)) qsort#(nil()) -> c_15() and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) GREATERS#(z0,nil()) -> c_3() LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) LOWERS#(z0,nil()) -> c_6() QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),lowers#(z0,z1),LOWERS#(z0,z1)) QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),greaters#(z0,z1),GREATERS#(z0,z1)) QSORT#(nil()) -> c_9() - Weak DPs: greaters#(z0,.(z1,z2)) -> c_10(greaters#(z0,z2),greaters#(z0,z2)) greaters#(z0,nil()) -> c_11() lowers#(z0,.(z1,z2)) -> c_12(lowers#(z0,z2),lowers#(z0,z2)) lowers#(z0,nil()) -> c_13() qsort#(.(z0,z1)) -> c_14(qsort#(lowers(z0,z1)),lowers#(z0,z1),qsort#(greaters(z0,z1)),greaters#(z0,z1)) qsort#(nil()) -> c_15() - Weak TRS: GREATERS(z0,.(z1,z2)) -> c7(GREATERS(z0,z2)) GREATERS(z0,.(z1,z2)) -> c8(GREATERS(z0,z2)) GREATERS(z0,nil()) -> c6() LOWERS(z0,.(z1,z2)) -> c4(LOWERS(z0,z2)) LOWERS(z0,.(z1,z2)) -> c5(LOWERS(z0,z2)) LOWERS(z0,nil()) -> c3() QSORT(.(z0,z1)) -> c1(QSORT(lowers(z0,z1)),LOWERS(z0,z1)) QSORT(.(z0,z1)) -> c2(QSORT(greaters(z0,z1)),GREATERS(z0,z1)) QSORT(nil()) -> c() greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() qsort(.(z0,z1)) -> ++(qsort(lowers(z0,z1)),.(z0,qsort(greaters(z0,z1)))) qsort(nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1,GREATERS#/2,LOWERS#/2,QSORT#/1,greaters#/2 ,lowers#/2,qsort#/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,if/3,nil/0,c_1/1,c_2/1 ,c_3/0,c_4/1,c_5/1,c_6/0,c_7/3,c_8/3,c_9/0,c_10/2,c_11/0,c_12/2,c_13/0,c_14/4,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS#,LOWERS#,QSORT#,greaters#,lowers# ,qsort#} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3,6,9} by application of Pre({3,6,9}) = {1,2,4,5,7,8}. Here rules are labelled as follows: 1: GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) 2: GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) 3: GREATERS#(z0,nil()) -> c_3() 4: LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) 5: LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) 6: LOWERS#(z0,nil()) -> c_6() 7: QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),lowers#(z0,z1),LOWERS#(z0,z1)) 8: QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),greaters#(z0,z1),GREATERS#(z0,z1)) 9: QSORT#(nil()) -> c_9() 10: greaters#(z0,.(z1,z2)) -> c_10(greaters#(z0,z2),greaters#(z0,z2)) 11: greaters#(z0,nil()) -> c_11() 12: lowers#(z0,.(z1,z2)) -> c_12(lowers#(z0,z2),lowers#(z0,z2)) 13: lowers#(z0,nil()) -> c_13() 14: qsort#(.(z0,z1)) -> c_14(qsort#(lowers(z0,z1)),lowers#(z0,z1),qsort#(greaters(z0,z1)),greaters#(z0,z1)) 15: qsort#(nil()) -> c_15() ** Step 1.b:3: RemoveWeakSuffixes. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),lowers#(z0,z1),LOWERS#(z0,z1)) QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),greaters#(z0,z1),GREATERS#(z0,z1)) - Weak DPs: GREATERS#(z0,nil()) -> c_3() LOWERS#(z0,nil()) -> c_6() QSORT#(nil()) -> c_9() greaters#(z0,.(z1,z2)) -> c_10(greaters#(z0,z2),greaters#(z0,z2)) greaters#(z0,nil()) -> c_11() lowers#(z0,.(z1,z2)) -> c_12(lowers#(z0,z2),lowers#(z0,z2)) lowers#(z0,nil()) -> c_13() qsort#(.(z0,z1)) -> c_14(qsort#(lowers(z0,z1)),lowers#(z0,z1),qsort#(greaters(z0,z1)),greaters#(z0,z1)) qsort#(nil()) -> c_15() - Weak TRS: GREATERS(z0,.(z1,z2)) -> c7(GREATERS(z0,z2)) GREATERS(z0,.(z1,z2)) -> c8(GREATERS(z0,z2)) GREATERS(z0,nil()) -> c6() LOWERS(z0,.(z1,z2)) -> c4(LOWERS(z0,z2)) LOWERS(z0,.(z1,z2)) -> c5(LOWERS(z0,z2)) LOWERS(z0,nil()) -> c3() QSORT(.(z0,z1)) -> c1(QSORT(lowers(z0,z1)),LOWERS(z0,z1)) QSORT(.(z0,z1)) -> c2(QSORT(greaters(z0,z1)),GREATERS(z0,z1)) QSORT(nil()) -> c() greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() qsort(.(z0,z1)) -> ++(qsort(lowers(z0,z1)),.(z0,qsort(greaters(z0,z1)))) qsort(nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1,GREATERS#/2,LOWERS#/2,QSORT#/1,greaters#/2 ,lowers#/2,qsort#/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,if/3,nil/0,c_1/1,c_2/1 ,c_3/0,c_4/1,c_5/1,c_6/0,c_7/3,c_8/3,c_9/0,c_10/2,c_11/0,c_12/2,c_13/0,c_14/4,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS#,LOWERS#,QSORT#,greaters#,lowers# ,qsort#} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) -->_1 GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)):2 -->_1 GREATERS#(z0,nil()) -> c_3():7 -->_1 GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)):1 2:S:GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) -->_1 GREATERS#(z0,nil()) -> c_3():7 -->_1 GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)):2 -->_1 GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)):1 3:S:LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) -->_1 LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)):4 -->_1 LOWERS#(z0,nil()) -> c_6():8 -->_1 LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)):3 4:S:LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) -->_1 LOWERS#(z0,nil()) -> c_6():8 -->_1 LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)):4 -->_1 LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)):3 5:S:QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),lowers#(z0,z1),LOWERS#(z0,z1)) -->_2 lowers#(z0,.(z1,z2)) -> c_12(lowers#(z0,z2),lowers#(z0,z2)):12 -->_1 QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),greaters#(z0,z1),GREATERS#(z0,z1)):6 -->_2 lowers#(z0,nil()) -> c_13():13 -->_1 QSORT#(nil()) -> c_9():9 -->_3 LOWERS#(z0,nil()) -> c_6():8 -->_1 QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),lowers#(z0,z1),LOWERS#(z0,z1)):5 -->_3 LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)):4 -->_3 LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)):3 6:S:QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),greaters#(z0,z1),GREATERS#(z0,z1)) -->_2 greaters#(z0,.(z1,z2)) -> c_10(greaters#(z0,z2),greaters#(z0,z2)):10 -->_2 greaters#(z0,nil()) -> c_11():11 -->_1 QSORT#(nil()) -> c_9():9 -->_3 GREATERS#(z0,nil()) -> c_3():7 -->_1 QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),greaters#(z0,z1),GREATERS#(z0,z1)):6 -->_1 QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),lowers#(z0,z1),LOWERS#(z0,z1)):5 -->_3 GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)):2 -->_3 GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)):1 7:W:GREATERS#(z0,nil()) -> c_3() 8:W:LOWERS#(z0,nil()) -> c_6() 9:W:QSORT#(nil()) -> c_9() 10:W:greaters#(z0,.(z1,z2)) -> c_10(greaters#(z0,z2),greaters#(z0,z2)) -->_2 greaters#(z0,nil()) -> c_11():11 -->_1 greaters#(z0,nil()) -> c_11():11 -->_2 greaters#(z0,.(z1,z2)) -> c_10(greaters#(z0,z2),greaters#(z0,z2)):10 -->_1 greaters#(z0,.(z1,z2)) -> c_10(greaters#(z0,z2),greaters#(z0,z2)):10 11:W:greaters#(z0,nil()) -> c_11() 12:W:lowers#(z0,.(z1,z2)) -> c_12(lowers#(z0,z2),lowers#(z0,z2)) -->_2 lowers#(z0,nil()) -> c_13():13 -->_1 lowers#(z0,nil()) -> c_13():13 -->_2 lowers#(z0,.(z1,z2)) -> c_12(lowers#(z0,z2),lowers#(z0,z2)):12 -->_1 lowers#(z0,.(z1,z2)) -> c_12(lowers#(z0,z2),lowers#(z0,z2)):12 13:W:lowers#(z0,nil()) -> c_13() 14:W:qsort#(.(z0,z1)) -> c_14(qsort#(lowers(z0,z1)),lowers#(z0,z1),qsort#(greaters(z0,z1)),greaters#(z0,z1)) -->_3 qsort#(nil()) -> c_15():15 -->_1 qsort#(nil()) -> c_15():15 -->_3 qsort#(.(z0,z1)) -> c_14(qsort#(lowers(z0,z1)) ,lowers#(z0,z1) ,qsort#(greaters(z0,z1)) ,greaters#(z0,z1)):14 -->_1 qsort#(.(z0,z1)) -> c_14(qsort#(lowers(z0,z1)) ,lowers#(z0,z1) ,qsort#(greaters(z0,z1)) ,greaters#(z0,z1)):14 -->_2 lowers#(z0,nil()) -> c_13():13 -->_2 lowers#(z0,.(z1,z2)) -> c_12(lowers#(z0,z2),lowers#(z0,z2)):12 -->_4 greaters#(z0,nil()) -> c_11():11 -->_4 greaters#(z0,.(z1,z2)) -> c_10(greaters#(z0,z2),greaters#(z0,z2)):10 15:W:qsort#(nil()) -> c_15() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 14: qsort#(.(z0,z1)) -> c_14(qsort#(lowers(z0,z1)) ,lowers#(z0,z1) ,qsort#(greaters(z0,z1)) ,greaters#(z0,z1)) 15: qsort#(nil()) -> c_15() 9: QSORT#(nil()) -> c_9() 10: greaters#(z0,.(z1,z2)) -> c_10(greaters#(z0,z2),greaters#(z0,z2)) 11: greaters#(z0,nil()) -> c_11() 12: lowers#(z0,.(z1,z2)) -> c_12(lowers#(z0,z2),lowers#(z0,z2)) 13: lowers#(z0,nil()) -> c_13() 8: LOWERS#(z0,nil()) -> c_6() 7: GREATERS#(z0,nil()) -> c_3() ** Step 1.b:4: SimplifyRHS. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),lowers#(z0,z1),LOWERS#(z0,z1)) QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),greaters#(z0,z1),GREATERS#(z0,z1)) - Weak TRS: GREATERS(z0,.(z1,z2)) -> c7(GREATERS(z0,z2)) GREATERS(z0,.(z1,z2)) -> c8(GREATERS(z0,z2)) GREATERS(z0,nil()) -> c6() LOWERS(z0,.(z1,z2)) -> c4(LOWERS(z0,z2)) LOWERS(z0,.(z1,z2)) -> c5(LOWERS(z0,z2)) LOWERS(z0,nil()) -> c3() QSORT(.(z0,z1)) -> c1(QSORT(lowers(z0,z1)),LOWERS(z0,z1)) QSORT(.(z0,z1)) -> c2(QSORT(greaters(z0,z1)),GREATERS(z0,z1)) QSORT(nil()) -> c() greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() qsort(.(z0,z1)) -> ++(qsort(lowers(z0,z1)),.(z0,qsort(greaters(z0,z1)))) qsort(nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1,GREATERS#/2,LOWERS#/2,QSORT#/1,greaters#/2 ,lowers#/2,qsort#/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,if/3,nil/0,c_1/1,c_2/1 ,c_3/0,c_4/1,c_5/1,c_6/0,c_7/3,c_8/3,c_9/0,c_10/2,c_11/0,c_12/2,c_13/0,c_14/4,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS#,LOWERS#,QSORT#,greaters#,lowers# ,qsort#} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) -->_1 GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)):2 -->_1 GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)):1 2:S:GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) -->_1 GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)):2 -->_1 GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)):1 3:S:LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) -->_1 LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)):4 -->_1 LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)):3 4:S:LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) -->_1 LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)):4 -->_1 LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)):3 5:S:QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),lowers#(z0,z1),LOWERS#(z0,z1)) -->_1 QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),greaters#(z0,z1),GREATERS#(z0,z1)):6 -->_1 QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),lowers#(z0,z1),LOWERS#(z0,z1)):5 -->_3 LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)):4 -->_3 LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)):3 6:S:QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),greaters#(z0,z1),GREATERS#(z0,z1)) -->_1 QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),greaters#(z0,z1),GREATERS#(z0,z1)):6 -->_1 QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),lowers#(z0,z1),LOWERS#(z0,z1)):5 -->_3 GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)):2 -->_3 GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),LOWERS#(z0,z1)) QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),GREATERS#(z0,z1)) ** Step 1.b:5: UsableRules. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),LOWERS#(z0,z1)) QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),GREATERS#(z0,z1)) - Weak TRS: GREATERS(z0,.(z1,z2)) -> c7(GREATERS(z0,z2)) GREATERS(z0,.(z1,z2)) -> c8(GREATERS(z0,z2)) GREATERS(z0,nil()) -> c6() LOWERS(z0,.(z1,z2)) -> c4(LOWERS(z0,z2)) LOWERS(z0,.(z1,z2)) -> c5(LOWERS(z0,z2)) LOWERS(z0,nil()) -> c3() QSORT(.(z0,z1)) -> c1(QSORT(lowers(z0,z1)),LOWERS(z0,z1)) QSORT(.(z0,z1)) -> c2(QSORT(greaters(z0,z1)),GREATERS(z0,z1)) QSORT(nil()) -> c() greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() qsort(.(z0,z1)) -> ++(qsort(lowers(z0,z1)),.(z0,qsort(greaters(z0,z1)))) qsort(nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1,GREATERS#/2,LOWERS#/2,QSORT#/1,greaters#/2 ,lowers#/2,qsort#/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,if/3,nil/0,c_1/1,c_2/1 ,c_3/0,c_4/1,c_5/1,c_6/0,c_7/2,c_8/2,c_9/0,c_10/2,c_11/0,c_12/2,c_13/0,c_14/4,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS#,LOWERS#,QSORT#,greaters#,lowers# ,qsort#} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),LOWERS#(z0,z1)) QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),GREATERS#(z0,z1)) ** Step 1.b:6: DecomposeDG. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),LOWERS#(z0,z1)) QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),GREATERS#(z0,z1)) - Weak TRS: greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1,GREATERS#/2,LOWERS#/2,QSORT#/1,greaters#/2 ,lowers#/2,qsort#/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,if/3,nil/0,c_1/1,c_2/1 ,c_3/0,c_4/1,c_5/1,c_6/0,c_7/2,c_8/2,c_9/0,c_10/2,c_11/0,c_12/2,c_13/0,c_14/4,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS#,LOWERS#,QSORT#,greaters#,lowers# ,qsort#} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + 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 QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),LOWERS#(z0,z1)) QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),GREATERS#(z0,z1)) and a lower component GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) Further, following extension rules are added to the lower component. QSORT#(.(z0,z1)) -> GREATERS#(z0,z1) QSORT#(.(z0,z1)) -> LOWERS#(z0,z1) QSORT#(.(z0,z1)) -> QSORT#(greaters(z0,z1)) QSORT#(.(z0,z1)) -> QSORT#(lowers(z0,z1)) *** Step 1.b:6.a:1: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),LOWERS#(z0,z1)) QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),GREATERS#(z0,z1)) - Weak TRS: greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1,GREATERS#/2,LOWERS#/2,QSORT#/1,greaters#/2 ,lowers#/2,qsort#/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,if/3,nil/0,c_1/1,c_2/1 ,c_3/0,c_4/1,c_5/1,c_6/0,c_7/2,c_8/2,c_9/0,c_10/2,c_11/0,c_12/2,c_13/0,c_14/4,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS#,LOWERS#,QSORT#,greaters#,lowers# ,qsort#} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),LOWERS#(z0,z1)) -->_1 QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),GREATERS#(z0,z1)):2 -->_1 QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),LOWERS#(z0,z1)):1 2:S:QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),GREATERS#(z0,z1)) -->_1 QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1)),GREATERS#(z0,z1)):2 -->_1 QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1)),LOWERS#(z0,z1)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1))) QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1))) *** Step 1.b:6.a:2: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1))) QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1))) - Weak TRS: greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1,GREATERS#/2,LOWERS#/2,QSORT#/1,greaters#/2 ,lowers#/2,qsort#/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,if/3,nil/0,c_1/1,c_2/1 ,c_3/0,c_4/1,c_5/1,c_6/0,c_7/1,c_8/1,c_9/0,c_10/2,c_11/0,c_12/2,c_13/0,c_14/4,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS#,LOWERS#,QSORT#,greaters#,lowers# ,qsort#} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + 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_7) = {1}, uargs(c_8) = {1} Following symbols are considered usable: {greaters,lowers,GREATERS#,LOWERS#,QSORT#,greaters#,lowers#,qsort#} TcT has computed the following interpretation: p(++) = [1] x1 + [1] x2 + [0] p(.) = [1] p(<=) = [1] x1 + [1] x2 + [0] p(GREATERS) = [0] p(LOWERS) = [0] p(QSORT) = [0] p(c) = [0] p(c1) = [1] x1 + [0] p(c2) = [0] p(c3) = [1] p(c4) = [4] p(c5) = [1] x1 + [2] p(c6) = [1] p(c7) = [0] p(c8) = [1] p(greaters) = [0] p(if) = [0] p(lowers) = [0] p(nil) = [0] p(qsort) = [1] p(GREATERS#) = [2] x1 + [0] p(LOWERS#) = [0] p(QSORT#) = [1] x1 + [0] p(greaters#) = [8] x1 + [2] x2 + [1] p(lowers#) = [0] p(qsort#) = [0] p(c_1) = [1] p(c_2) = [2] x1 + [1] p(c_3) = [1] p(c_4) = [0] p(c_5) = [0] p(c_6) = [2] p(c_7) = [4] x1 + [1] p(c_8) = [4] x1 + [0] p(c_9) = [2] p(c_10) = [1] x2 + [8] p(c_11) = [1] p(c_12) = [4] x1 + [1] p(c_13) = [0] p(c_14) = [1] x2 + [0] p(c_15) = [1] Following rules are strictly oriented: QSORT#(.(z0,z1)) = [1] > [0] = c_8(QSORT#(greaters(z0,z1))) Following rules are (at-least) weakly oriented: QSORT#(.(z0,z1)) = [1] >= [1] = c_7(QSORT#(lowers(z0,z1))) greaters(z0,.(z1,z2)) = [0] >= [0] = if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) = [0] >= [0] = nil() lowers(z0,.(z1,z2)) = [0] >= [0] = if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) = [0] >= [0] = nil() *** Step 1.b:6.a:3: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1))) - Weak DPs: QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1))) - Weak TRS: greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1,GREATERS#/2,LOWERS#/2,QSORT#/1,greaters#/2 ,lowers#/2,qsort#/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,if/3,nil/0,c_1/1,c_2/1 ,c_3/0,c_4/1,c_5/1,c_6/0,c_7/1,c_8/1,c_9/0,c_10/2,c_11/0,c_12/2,c_13/0,c_14/4,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS#,LOWERS#,QSORT#,greaters#,lowers# ,qsort#} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + 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_7) = {1}, uargs(c_8) = {1} Following symbols are considered usable: {greaters,lowers,GREATERS#,LOWERS#,QSORT#,greaters#,lowers#,qsort#} TcT has computed the following interpretation: p(++) = [1] x1 + [1] x2 + [0] p(.) = [8] p(<=) = [0] p(GREATERS) = [0] p(LOWERS) = [0] p(QSORT) = [0] p(c) = [0] p(c1) = [1] x1 + [1] x2 + [0] p(c2) = [1] x1 + [1] x2 + [0] p(c3) = [0] p(c4) = [1] x1 + [0] p(c5) = [1] x1 + [0] p(c6) = [0] p(c7) = [1] x1 + [0] p(c8) = [1] x1 + [0] p(greaters) = [0] p(if) = [1] x1 + [0] p(lowers) = [0] p(nil) = [0] p(qsort) = [0] p(GREATERS#) = [1] x2 + [1] p(LOWERS#) = [8] x2 + [1] p(QSORT#) = [2] x1 + [0] p(greaters#) = [4] x1 + [4] x2 + [0] p(lowers#) = [2] x1 + [1] x2 + [1] p(qsort#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [2] p(c_4) = [8] x1 + [1] p(c_5) = [1] x1 + [1] p(c_6) = [2] p(c_7) = [8] x1 + [8] p(c_8) = [2] x1 + [4] p(c_9) = [2] p(c_10) = [1] x1 + [1] x2 + [1] p(c_11) = [1] p(c_12) = [1] x2 + [0] p(c_13) = [1] p(c_14) = [1] x1 + [1] x2 + [2] x3 + [2] x4 + [1] p(c_15) = [1] Following rules are strictly oriented: QSORT#(.(z0,z1)) = [16] > [8] = c_7(QSORT#(lowers(z0,z1))) Following rules are (at-least) weakly oriented: QSORT#(.(z0,z1)) = [16] >= [4] = c_8(QSORT#(greaters(z0,z1))) greaters(z0,.(z1,z2)) = [0] >= [0] = if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) = [0] >= [0] = nil() lowers(z0,.(z1,z2)) = [0] >= [0] = if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) = [0] >= [0] = nil() *** Step 1.b:6.a:4: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: QSORT#(.(z0,z1)) -> c_7(QSORT#(lowers(z0,z1))) QSORT#(.(z0,z1)) -> c_8(QSORT#(greaters(z0,z1))) - Weak TRS: greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1,GREATERS#/2,LOWERS#/2,QSORT#/1,greaters#/2 ,lowers#/2,qsort#/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,if/3,nil/0,c_1/1,c_2/1 ,c_3/0,c_4/1,c_5/1,c_6/0,c_7/1,c_8/1,c_9/0,c_10/2,c_11/0,c_12/2,c_13/0,c_14/4,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS#,LOWERS#,QSORT#,greaters#,lowers# ,qsort#} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + 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^1)) + Considered Problem: - Strict DPs: GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) - Weak DPs: QSORT#(.(z0,z1)) -> GREATERS#(z0,z1) QSORT#(.(z0,z1)) -> LOWERS#(z0,z1) QSORT#(.(z0,z1)) -> QSORT#(greaters(z0,z1)) QSORT#(.(z0,z1)) -> QSORT#(lowers(z0,z1)) - Weak TRS: greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1,GREATERS#/2,LOWERS#/2,QSORT#/1,greaters#/2 ,lowers#/2,qsort#/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,if/3,nil/0,c_1/1,c_2/1 ,c_3/0,c_4/1,c_5/1,c_6/0,c_7/2,c_8/2,c_9/0,c_10/2,c_11/0,c_12/2,c_13/0,c_14/4,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS#,LOWERS#,QSORT#,greaters#,lowers# ,qsort#} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + 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_1) = {1}, uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1} Following symbols are considered usable: {greaters,lowers,GREATERS#,LOWERS#,QSORT#,greaters#,lowers#,qsort#} TcT has computed the following interpretation: p(++) = [2] p(.) = [1] x2 + [1] p(<=) = [0] p(GREATERS) = [1] x1 + [1] x2 + [0] p(LOWERS) = [4] x1 + [1] x2 + [2] p(QSORT) = [2] x1 + [0] p(c) = [0] p(c1) = [1] x2 + [1] p(c2) = [1] p(c3) = [1] p(c4) = [1] p(c5) = [0] p(c6) = [0] p(c7) = [1] x1 + [0] p(c8) = [0] p(greaters) = [1] x2 + [1] p(if) = [1] x1 + [0] p(lowers) = [0] p(nil) = [0] p(qsort) = [2] x1 + [1] p(GREATERS#) = [0] p(LOWERS#) = [4] x2 + [0] p(QSORT#) = [4] x1 + [0] p(greaters#) = [1] x1 + [2] x2 + [0] p(lowers#) = [1] x1 + [8] x2 + [8] p(qsort#) = [1] x1 + [1] p(c_1) = [8] x1 + [0] p(c_2) = [2] x1 + [0] p(c_3) = [2] p(c_4) = [1] x1 + [2] p(c_5) = [1] x1 + [4] p(c_6) = [0] p(c_7) = [1] x1 + [1] p(c_8) = [1] x2 + [1] p(c_9) = [1] p(c_10) = [1] x2 + [2] p(c_11) = [2] p(c_12) = [1] x1 + [2] x2 + [1] p(c_13) = [2] p(c_14) = [1] x1 + [1] x3 + [1] x4 + [0] p(c_15) = [2] Following rules are strictly oriented: LOWERS#(z0,.(z1,z2)) = [4] z2 + [4] > [4] z2 + [2] = c_4(LOWERS#(z0,z2)) Following rules are (at-least) weakly oriented: GREATERS#(z0,.(z1,z2)) = [0] >= [0] = c_1(GREATERS#(z0,z2)) GREATERS#(z0,.(z1,z2)) = [0] >= [0] = c_2(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) = [4] z2 + [4] >= [4] z2 + [4] = c_5(LOWERS#(z0,z2)) QSORT#(.(z0,z1)) = [4] z1 + [4] >= [0] = GREATERS#(z0,z1) QSORT#(.(z0,z1)) = [4] z1 + [4] >= [4] z1 + [0] = LOWERS#(z0,z1) QSORT#(.(z0,z1)) = [4] z1 + [4] >= [4] z1 + [4] = QSORT#(greaters(z0,z1)) QSORT#(.(z0,z1)) = [4] z1 + [4] >= [0] = QSORT#(lowers(z0,z1)) greaters(z0,.(z1,z2)) = [1] z2 + [2] >= [0] = if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) = [1] >= [0] = nil() lowers(z0,.(z1,z2)) = [0] >= [0] = if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) = [0] >= [0] = nil() *** Step 1.b:6.b:2: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) - Weak DPs: LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) QSORT#(.(z0,z1)) -> GREATERS#(z0,z1) QSORT#(.(z0,z1)) -> LOWERS#(z0,z1) QSORT#(.(z0,z1)) -> QSORT#(greaters(z0,z1)) QSORT#(.(z0,z1)) -> QSORT#(lowers(z0,z1)) - Weak TRS: greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1,GREATERS#/2,LOWERS#/2,QSORT#/1,greaters#/2 ,lowers#/2,qsort#/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,if/3,nil/0,c_1/1,c_2/1 ,c_3/0,c_4/1,c_5/1,c_6/0,c_7/2,c_8/2,c_9/0,c_10/2,c_11/0,c_12/2,c_13/0,c_14/4,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS#,LOWERS#,QSORT#,greaters#,lowers# ,qsort#} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + 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_1) = {1}, uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1} Following symbols are considered usable: {greaters,lowers,GREATERS#,LOWERS#,QSORT#,greaters#,lowers#,qsort#} TcT has computed the following interpretation: p(++) = [1] x1 + [1] x2 + [0] p(.) = [1] x2 + [8] p(<=) = [1] x1 + [1] x2 + [0] p(GREATERS) = [0] p(LOWERS) = [0] p(QSORT) = [0] p(c) = [0] p(c1) = [1] x1 + [1] x2 + [0] p(c2) = [1] x1 + [1] x2 + [0] p(c3) = [0] p(c4) = [1] x1 + [0] p(c5) = [0] p(c6) = [4] p(c7) = [8] p(c8) = [8] p(greaters) = [5] p(if) = [2] p(lowers) = [1] x2 + [4] p(nil) = [0] p(qsort) = [0] p(GREATERS#) = [1] x2 + [0] p(LOWERS#) = [0] p(QSORT#) = [2] x1 + [0] p(greaters#) = [1] p(lowers#) = [1] x1 + [1] x2 + [4] p(qsort#) = [1] x1 + [1] p(c_1) = [1] x1 + [0] p(c_2) = [1] x1 + [8] p(c_3) = [4] p(c_4) = [8] x1 + [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] p(c_7) = [1] x2 + [2] p(c_8) = [0] p(c_9) = [1] p(c_10) = [2] x2 + [1] p(c_11) = [4] p(c_12) = [8] x1 + [1] p(c_13) = [2] p(c_14) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] p(c_15) = [1] Following rules are strictly oriented: GREATERS#(z0,.(z1,z2)) = [1] z2 + [8] > [1] z2 + [0] = c_1(GREATERS#(z0,z2)) Following rules are (at-least) weakly oriented: GREATERS#(z0,.(z1,z2)) = [1] z2 + [8] >= [1] z2 + [8] = c_2(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) = [0] >= [0] = c_4(LOWERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) = [0] >= [0] = c_5(LOWERS#(z0,z2)) QSORT#(.(z0,z1)) = [2] z1 + [16] >= [1] z1 + [0] = GREATERS#(z0,z1) QSORT#(.(z0,z1)) = [2] z1 + [16] >= [0] = LOWERS#(z0,z1) QSORT#(.(z0,z1)) = [2] z1 + [16] >= [10] = QSORT#(greaters(z0,z1)) QSORT#(.(z0,z1)) = [2] z1 + [16] >= [2] z1 + [8] = QSORT#(lowers(z0,z1)) greaters(z0,.(z1,z2)) = [5] >= [2] = if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) = [5] >= [0] = nil() lowers(z0,.(z1,z2)) = [1] z2 + [12] >= [2] = if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) = [4] >= [0] = nil() *** Step 1.b:6.b:3: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) - Weak DPs: GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) QSORT#(.(z0,z1)) -> GREATERS#(z0,z1) QSORT#(.(z0,z1)) -> LOWERS#(z0,z1) QSORT#(.(z0,z1)) -> QSORT#(greaters(z0,z1)) QSORT#(.(z0,z1)) -> QSORT#(lowers(z0,z1)) - Weak TRS: greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1,GREATERS#/2,LOWERS#/2,QSORT#/1,greaters#/2 ,lowers#/2,qsort#/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,if/3,nil/0,c_1/1,c_2/1 ,c_3/0,c_4/1,c_5/1,c_6/0,c_7/2,c_8/2,c_9/0,c_10/2,c_11/0,c_12/2,c_13/0,c_14/4,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS#,LOWERS#,QSORT#,greaters#,lowers# ,qsort#} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + 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_1) = {1}, uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1} Following symbols are considered usable: {greaters,lowers,GREATERS#,LOWERS#,QSORT#,greaters#,lowers#,qsort#} TcT has computed the following interpretation: p(++) = [1] x1 + [0] p(.) = [1] x1 + [1] x2 + [10] p(<=) = [0] p(GREATERS) = [0] p(LOWERS) = [0] p(QSORT) = [0] p(c) = [0] p(c1) = [1] x1 + [1] x2 + [0] p(c2) = [1] x1 + [1] x2 + [0] p(c3) = [0] p(c4) = [1] x1 + [0] p(c5) = [1] x1 + [0] p(c6) = [0] p(c7) = [1] x1 + [0] p(c8) = [1] x1 + [0] p(greaters) = [1] x1 + [1] x2 + [3] p(if) = [1] x1 + [13] p(lowers) = [1] x2 + [3] p(nil) = [0] p(qsort) = [0] p(GREATERS#) = [0] p(LOWERS#) = [3] x1 + [1] x2 + [0] p(QSORT#) = [3] x1 + [0] p(greaters#) = [0] p(lowers#) = [0] p(qsort#) = [0] p(c_1) = [4] x1 + [0] p(c_2) = [8] x1 + [0] p(c_3) = [0] p(c_4) = [1] x1 + [10] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [4] x1 + [0] p(c_13) = [0] p(c_14) = [2] x3 + [0] p(c_15) = [0] Following rules are strictly oriented: LOWERS#(z0,.(z1,z2)) = [3] z0 + [1] z1 + [1] z2 + [10] > [3] z0 + [1] z2 + [0] = c_5(LOWERS#(z0,z2)) Following rules are (at-least) weakly oriented: GREATERS#(z0,.(z1,z2)) = [0] >= [0] = c_1(GREATERS#(z0,z2)) GREATERS#(z0,.(z1,z2)) = [0] >= [0] = c_2(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) = [3] z0 + [1] z1 + [1] z2 + [10] >= [3] z0 + [1] z2 + [10] = c_4(LOWERS#(z0,z2)) QSORT#(.(z0,z1)) = [3] z0 + [3] z1 + [30] >= [0] = GREATERS#(z0,z1) QSORT#(.(z0,z1)) = [3] z0 + [3] z1 + [30] >= [3] z0 + [1] z1 + [0] = LOWERS#(z0,z1) QSORT#(.(z0,z1)) = [3] z0 + [3] z1 + [30] >= [3] z0 + [3] z1 + [9] = QSORT#(greaters(z0,z1)) QSORT#(.(z0,z1)) = [3] z0 + [3] z1 + [30] >= [3] z1 + [9] = QSORT#(lowers(z0,z1)) greaters(z0,.(z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [13] >= [13] = if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) = [1] z0 + [3] >= [0] = nil() lowers(z0,.(z1,z2)) = [1] z1 + [1] z2 + [13] >= [13] = if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) = [3] >= [0] = nil() *** Step 1.b:6.b:4: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) - Weak DPs: GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) QSORT#(.(z0,z1)) -> GREATERS#(z0,z1) QSORT#(.(z0,z1)) -> LOWERS#(z0,z1) QSORT#(.(z0,z1)) -> QSORT#(greaters(z0,z1)) QSORT#(.(z0,z1)) -> QSORT#(lowers(z0,z1)) - Weak TRS: greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1,GREATERS#/2,LOWERS#/2,QSORT#/1,greaters#/2 ,lowers#/2,qsort#/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,if/3,nil/0,c_1/1,c_2/1 ,c_3/0,c_4/1,c_5/1,c_6/0,c_7/2,c_8/2,c_9/0,c_10/2,c_11/0,c_12/2,c_13/0,c_14/4,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS#,LOWERS#,QSORT#,greaters#,lowers# ,qsort#} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + 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_1) = {1}, uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1} Following symbols are considered usable: {greaters,lowers,GREATERS#,LOWERS#,QSORT#,greaters#,lowers#,qsort#} TcT has computed the following interpretation: p(++) = [1] x2 + [2] p(.) = [1] x1 + [1] x2 + [2] p(<=) = [0] p(GREATERS) = [1] x2 + [4] p(LOWERS) = [1] x1 + [1] p(QSORT) = [0] p(c) = [1] p(c1) = [1] x1 + [1] x2 + [0] p(c2) = [1] p(c3) = [1] p(c4) = [0] p(c5) = [4] p(c6) = [0] p(c7) = [1] p(c8) = [1] x1 + [2] p(greaters) = [0] p(if) = [1] x1 + [0] p(lowers) = [0] p(nil) = [0] p(qsort) = [1] x1 + [2] p(GREATERS#) = [8] x2 + [0] p(LOWERS#) = [0] p(QSORT#) = [8] x1 + [0] p(greaters#) = [1] x1 + [4] p(lowers#) = [2] p(qsort#) = [4] p(c_1) = [1] x1 + [0] p(c_2) = [1] x1 + [8] p(c_3) = [1] p(c_4) = [4] x1 + [0] p(c_5) = [8] x1 + [0] p(c_6) = [0] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [4] x1 + [2] p(c_9) = [1] p(c_10) = [2] x2 + [1] p(c_11) = [0] p(c_12) = [1] x1 + [0] p(c_13) = [1] p(c_14) = [8] x2 + [1] x3 + [1] x4 + [1] p(c_15) = [0] Following rules are strictly oriented: GREATERS#(z0,.(z1,z2)) = [8] z1 + [8] z2 + [16] > [8] z2 + [8] = c_2(GREATERS#(z0,z2)) Following rules are (at-least) weakly oriented: GREATERS#(z0,.(z1,z2)) = [8] z1 + [8] z2 + [16] >= [8] z2 + [0] = c_1(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) = [0] >= [0] = c_4(LOWERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) = [0] >= [0] = c_5(LOWERS#(z0,z2)) QSORT#(.(z0,z1)) = [8] z0 + [8] z1 + [16] >= [8] z1 + [0] = GREATERS#(z0,z1) QSORT#(.(z0,z1)) = [8] z0 + [8] z1 + [16] >= [0] = LOWERS#(z0,z1) QSORT#(.(z0,z1)) = [8] z0 + [8] z1 + [16] >= [0] = QSORT#(greaters(z0,z1)) QSORT#(.(z0,z1)) = [8] z0 + [8] z1 + [16] >= [0] = QSORT#(lowers(z0,z1)) greaters(z0,.(z1,z2)) = [0] >= [0] = if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) = [0] >= [0] = nil() lowers(z0,.(z1,z2)) = [0] >= [0] = if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) = [0] >= [0] = nil() *** Step 1.b:6.b:5: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: GREATERS#(z0,.(z1,z2)) -> c_1(GREATERS#(z0,z2)) GREATERS#(z0,.(z1,z2)) -> c_2(GREATERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_4(LOWERS#(z0,z2)) LOWERS#(z0,.(z1,z2)) -> c_5(LOWERS#(z0,z2)) QSORT#(.(z0,z1)) -> GREATERS#(z0,z1) QSORT#(.(z0,z1)) -> LOWERS#(z0,z1) QSORT#(.(z0,z1)) -> QSORT#(greaters(z0,z1)) QSORT#(.(z0,z1)) -> QSORT#(lowers(z0,z1)) - Weak TRS: greaters(z0,.(z1,z2)) -> if(<=(z1,z0),greaters(z0,z2),.(z1,greaters(z0,z2))) greaters(z0,nil()) -> nil() lowers(z0,.(z1,z2)) -> if(<=(z1,z0),.(z1,lowers(z0,z2)),lowers(z0,z2)) lowers(z0,nil()) -> nil() - Signature: {GREATERS/2,LOWERS/2,QSORT/1,greaters/2,lowers/2,qsort/1,GREATERS#/2,LOWERS#/2,QSORT#/1,greaters#/2 ,lowers#/2,qsort#/1} / {++/2,./2,<=/2,c/0,c1/2,c2/2,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,if/3,nil/0,c_1/1,c_2/1 ,c_3/0,c_4/1,c_5/1,c_6/0,c_7/2,c_8/2,c_9/0,c_10/2,c_11/0,c_12/2,c_13/0,c_14/4,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {GREATERS#,LOWERS#,QSORT#,greaters#,lowers# ,qsort#} and constructors {++,.,<=,c,c1,c2,c3,c4,c5,c6,c7,c8,if,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^2))