WORST_CASE(Omega(n^1),O(n^3)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^3)) + Considered Problem: - Strict TRS: APPEND(add(z0,z1),z2) -> c4(APPEND(z1,z2)) APPEND(nil(),z0) -> c3() F_1(pair(z0,z1),z2,z3,z4) -> c7(F_2(lt(z2,z3),z2,z3,z4,z0,z1),LT(z2,z3)) F_2(false(),z0,z1,z2,z3,z4) -> c9() F_2(true(),z0,z1,z2,z3,z4) -> c8() F_3(pair(z0,z1),z2,z3) -> c12(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z0)) F_3(pair(z0,z1),z2,z3) -> c13(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z1)) LT(0(),s(z0)) -> c() LT(s(z0),0()) -> c1() LT(s(z0),s(z1)) -> c2(LT(z0,z1)) QSORT(add(z0,z1)) -> c11(F_3(split(z0,z1),z0,z1),SPLIT(z0,z1)) QSORT(nil()) -> c10() SPLIT(z0,add(z1,z2)) -> c6(F_1(split(z0,z2),z0,z1,z2),SPLIT(z0,z2)) SPLIT(z0,nil()) -> c5() - Weak TRS: append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND,F_1,F_2,F_3,LT,QSORT,SPLIT,append,f_1,f_2,f_3,lt ,qsort,split} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil,pair,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APPEND(add(z0,z1),z2) -> c4(APPEND(z1,z2)) APPEND(nil(),z0) -> c3() F_1(pair(z0,z1),z2,z3,z4) -> c7(F_2(lt(z2,z3),z2,z3,z4,z0,z1),LT(z2,z3)) F_2(false(),z0,z1,z2,z3,z4) -> c9() F_2(true(),z0,z1,z2,z3,z4) -> c8() F_3(pair(z0,z1),z2,z3) -> c12(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z0)) F_3(pair(z0,z1),z2,z3) -> c13(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z1)) LT(0(),s(z0)) -> c() LT(s(z0),0()) -> c1() LT(s(z0),s(z1)) -> c2(LT(z0,z1)) QSORT(add(z0,z1)) -> c11(F_3(split(z0,z1),z0,z1),SPLIT(z0,z1)) QSORT(nil()) -> c10() SPLIT(z0,add(z1,z2)) -> c6(F_1(split(z0,z2),z0,z1,z2),SPLIT(z0,z2)) SPLIT(z0,nil()) -> c5() - Weak TRS: append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND,F_1,F_2,F_3,LT,QSORT,SPLIT,append,f_1,f_2,f_3,lt ,qsort,split} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil,pair,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APPEND(add(z0,z1),z2) -> c4(APPEND(z1,z2)) APPEND(nil(),z0) -> c3() F_1(pair(z0,z1),z2,z3,z4) -> c7(F_2(lt(z2,z3),z2,z3,z4,z0,z1),LT(z2,z3)) F_2(false(),z0,z1,z2,z3,z4) -> c9() F_2(true(),z0,z1,z2,z3,z4) -> c8() F_3(pair(z0,z1),z2,z3) -> c12(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z0)) F_3(pair(z0,z1),z2,z3) -> c13(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z1)) LT(0(),s(z0)) -> c() LT(s(z0),0()) -> c1() LT(s(z0),s(z1)) -> c2(LT(z0,z1)) QSORT(add(z0,z1)) -> c11(F_3(split(z0,z1),z0,z1),SPLIT(z0,z1)) QSORT(nil()) -> c10() SPLIT(z0,add(z1,z2)) -> c6(F_1(split(z0,z2),z0,z1,z2),SPLIT(z0,z2)) SPLIT(z0,nil()) -> c5() - Weak TRS: append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND,F_1,F_2,F_3,LT,QSORT,SPLIT,append,f_1,f_2,f_3,lt ,qsort,split} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil,pair,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: APPEND(y,z){y -> add(x,y)} = APPEND(add(x,y),z) ->^+ c4(APPEND(y,z)) = C[APPEND(y,z) = APPEND(y,z){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: APPEND(add(z0,z1),z2) -> c4(APPEND(z1,z2)) APPEND(nil(),z0) -> c3() F_1(pair(z0,z1),z2,z3,z4) -> c7(F_2(lt(z2,z3),z2,z3,z4,z0,z1),LT(z2,z3)) F_2(false(),z0,z1,z2,z3,z4) -> c9() F_2(true(),z0,z1,z2,z3,z4) -> c8() F_3(pair(z0,z1),z2,z3) -> c12(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z0)) F_3(pair(z0,z1),z2,z3) -> c13(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z1)) LT(0(),s(z0)) -> c() LT(s(z0),0()) -> c1() LT(s(z0),s(z1)) -> c2(LT(z0,z1)) QSORT(add(z0,z1)) -> c11(F_3(split(z0,z1),z0,z1),SPLIT(z0,z1)) QSORT(nil()) -> c10() SPLIT(z0,add(z1,z2)) -> c6(F_1(split(z0,z2),z0,z1,z2),SPLIT(z0,z2)) SPLIT(z0,nil()) -> c5() - Weak TRS: append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND,F_1,F_2,F_3,LT,QSORT,SPLIT,append,f_1,f_2,f_3,lt ,qsort,split} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil,pair,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) APPEND#(nil(),z0) -> c_2() F_1#(pair(z0,z1),z2,z3,z4) -> c_3(F_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3),LT#(z2,z3)) F_2#(false(),z0,z1,z2,z3,z4) -> c_4() F_2#(true(),z0,z1,z2,z3,z4) -> c_5() F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1),QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1),QSORT#(z1)) LT#(0(),s(z0)) -> c_8() LT#(s(z0),0()) -> c_9() LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),split#(z0,z1),SPLIT#(z0,z1)) QSORT#(nil()) -> c_12() SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),split#(z0,z2),SPLIT#(z0,z2)) SPLIT#(z0,nil()) -> c_14() Weak DPs append#(add(z0,z1),z2) -> c_15(append#(z1,z2)) append#(nil(),z0) -> c_16() f_1#(pair(z0,z1),z2,z3,z4) -> c_17(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) f_2#(false(),z0,z1,z2,z3,z4) -> c_18() f_2#(true(),z0,z1,z2,z3,z4) -> c_19() f_3#(pair(z0,z1),z2,z3) -> c_20(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) lt#(0(),s(z0)) -> c_21() lt#(s(z0),0()) -> c_22() lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)) qsort#(add(z0,z1)) -> c_24(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) qsort#(nil()) -> c_25() split#(z0,add(z1,z2)) -> c_26(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) split#(z0,nil()) -> c_27() and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) APPEND#(nil(),z0) -> c_2() F_1#(pair(z0,z1),z2,z3,z4) -> c_3(F_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3),LT#(z2,z3)) F_2#(false(),z0,z1,z2,z3,z4) -> c_4() F_2#(true(),z0,z1,z2,z3,z4) -> c_5() F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1),QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1),QSORT#(z1)) LT#(0(),s(z0)) -> c_8() LT#(s(z0),0()) -> c_9() LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),split#(z0,z1),SPLIT#(z0,z1)) QSORT#(nil()) -> c_12() SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),split#(z0,z2),SPLIT#(z0,z2)) SPLIT#(z0,nil()) -> c_14() - Weak DPs: append#(add(z0,z1),z2) -> c_15(append#(z1,z2)) append#(nil(),z0) -> c_16() f_1#(pair(z0,z1),z2,z3,z4) -> c_17(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) f_2#(false(),z0,z1,z2,z3,z4) -> c_18() f_2#(true(),z0,z1,z2,z3,z4) -> c_19() f_3#(pair(z0,z1),z2,z3) -> c_20(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) lt#(0(),s(z0)) -> c_21() lt#(s(z0),0()) -> c_22() lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)) qsort#(add(z0,z1)) -> c_24(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) qsort#(nil()) -> c_25() split#(z0,add(z1,z2)) -> c_26(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) split#(z0,nil()) -> c_27() - Weak TRS: APPEND(add(z0,z1),z2) -> c4(APPEND(z1,z2)) APPEND(nil(),z0) -> c3() F_1(pair(z0,z1),z2,z3,z4) -> c7(F_2(lt(z2,z3),z2,z3,z4,z0,z1),LT(z2,z3)) F_2(false(),z0,z1,z2,z3,z4) -> c9() F_2(true(),z0,z1,z2,z3,z4) -> c8() F_3(pair(z0,z1),z2,z3) -> c12(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z0)) F_3(pair(z0,z1),z2,z3) -> c13(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z1)) LT(0(),s(z0)) -> c() LT(s(z0),0()) -> c1() LT(s(z0),s(z1)) -> c2(LT(z0,z1)) QSORT(add(z0,z1)) -> c11(F_3(split(z0,z1),z0,z1),SPLIT(z0,z1)) QSORT(nil()) -> c10() SPLIT(z0,add(z1,z2)) -> c6(F_1(split(z0,z2),z0,z1,z2),SPLIT(z0,z2)) SPLIT(z0,nil()) -> c5() append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/4,c_7/4,c_8/0,c_9/0,c_10/1,c_11/3,c_12/0,c_13/3,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,4,5,8,9,12,14} by application of Pre({2,4,5,8,9,12,14}) = {1,3,6,7,10,11,13}. Here rules are labelled as follows: 1: APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) 2: APPEND#(nil(),z0) -> c_2() 3: F_1#(pair(z0,z1),z2,z3,z4) -> c_3(F_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3),LT#(z2,z3)) 4: F_2#(false(),z0,z1,z2,z3,z4) -> c_4() 5: F_2#(true(),z0,z1,z2,z3,z4) -> c_5() 6: F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1),QSORT#(z0)) 7: F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1),QSORT#(z1)) 8: LT#(0(),s(z0)) -> c_8() 9: LT#(s(z0),0()) -> c_9() 10: LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) 11: QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),split#(z0,z1),SPLIT#(z0,z1)) 12: QSORT#(nil()) -> c_12() 13: SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),split#(z0,z2),SPLIT#(z0,z2)) 14: SPLIT#(z0,nil()) -> c_14() 15: append#(add(z0,z1),z2) -> c_15(append#(z1,z2)) 16: append#(nil(),z0) -> c_16() 17: f_1#(pair(z0,z1),z2,z3,z4) -> c_17(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) 18: f_2#(false(),z0,z1,z2,z3,z4) -> c_18() 19: f_2#(true(),z0,z1,z2,z3,z4) -> c_19() 20: f_3#(pair(z0,z1),z2,z3) -> c_20(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) 21: lt#(0(),s(z0)) -> c_21() 22: lt#(s(z0),0()) -> c_22() 23: lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)) 24: qsort#(add(z0,z1)) -> c_24(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) 25: qsort#(nil()) -> c_25() 26: split#(z0,add(z1,z2)) -> c_26(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) 27: split#(z0,nil()) -> c_27() ** Step 1.b:3: RemoveWeakSuffixes. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) F_1#(pair(z0,z1),z2,z3,z4) -> c_3(F_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3),LT#(z2,z3)) F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1),QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1),QSORT#(z1)) LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),split#(z0,z1),SPLIT#(z0,z1)) SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),split#(z0,z2),SPLIT#(z0,z2)) - Weak DPs: APPEND#(nil(),z0) -> c_2() F_2#(false(),z0,z1,z2,z3,z4) -> c_4() F_2#(true(),z0,z1,z2,z3,z4) -> c_5() LT#(0(),s(z0)) -> c_8() LT#(s(z0),0()) -> c_9() QSORT#(nil()) -> c_12() SPLIT#(z0,nil()) -> c_14() append#(add(z0,z1),z2) -> c_15(append#(z1,z2)) append#(nil(),z0) -> c_16() f_1#(pair(z0,z1),z2,z3,z4) -> c_17(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) f_2#(false(),z0,z1,z2,z3,z4) -> c_18() f_2#(true(),z0,z1,z2,z3,z4) -> c_19() f_3#(pair(z0,z1),z2,z3) -> c_20(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) lt#(0(),s(z0)) -> c_21() lt#(s(z0),0()) -> c_22() lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)) qsort#(add(z0,z1)) -> c_24(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) qsort#(nil()) -> c_25() split#(z0,add(z1,z2)) -> c_26(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) split#(z0,nil()) -> c_27() - Weak TRS: APPEND(add(z0,z1),z2) -> c4(APPEND(z1,z2)) APPEND(nil(),z0) -> c3() F_1(pair(z0,z1),z2,z3,z4) -> c7(F_2(lt(z2,z3),z2,z3,z4,z0,z1),LT(z2,z3)) F_2(false(),z0,z1,z2,z3,z4) -> c9() F_2(true(),z0,z1,z2,z3,z4) -> c8() F_3(pair(z0,z1),z2,z3) -> c12(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z0)) F_3(pair(z0,z1),z2,z3) -> c13(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z1)) LT(0(),s(z0)) -> c() LT(s(z0),0()) -> c1() LT(s(z0),s(z1)) -> c2(LT(z0,z1)) QSORT(add(z0,z1)) -> c11(F_3(split(z0,z1),z0,z1),SPLIT(z0,z1)) QSORT(nil()) -> c10() SPLIT(z0,add(z1,z2)) -> c6(F_1(split(z0,z2),z0,z1,z2),SPLIT(z0,z2)) SPLIT(z0,nil()) -> c5() append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/4,c_7/4,c_8/0,c_9/0,c_10/1,c_11/3,c_12/0,c_13/3,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) -->_1 APPEND#(nil(),z0) -> c_2():8 -->_1 APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)):1 2:S:F_1#(pair(z0,z1),z2,z3,z4) -> c_3(F_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3),LT#(z2,z3)) -->_2 lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)):23 -->_3 LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)):5 -->_2 lt#(s(z0),0()) -> c_22():22 -->_2 lt#(0(),s(z0)) -> c_21():21 -->_3 LT#(s(z0),0()) -> c_9():12 -->_3 LT#(0(),s(z0)) -> c_8():11 -->_1 F_2#(true(),z0,z1,z2,z3,z4) -> c_5():10 -->_1 F_2#(false(),z0,z1,z2,z3,z4) -> c_4():9 3:S:F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1),QSORT#(z0)) -->_3 qsort#(add(z0,z1)) -> c_24(f_3#(split(z0,z1),z0,z1),split#(z0,z1)):24 -->_2 qsort#(add(z0,z1)) -> c_24(f_3#(split(z0,z1),z0,z1),split#(z0,z1)):24 -->_4 QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),split#(z0,z1),SPLIT#(z0,z1)):6 -->_3 qsort#(nil()) -> c_25():25 -->_2 qsort#(nil()) -> c_25():25 -->_4 QSORT#(nil()) -> c_12():13 -->_1 APPEND#(nil(),z0) -> c_2():8 -->_1 APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)):1 4:S:F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1),QSORT#(z1)) -->_3 qsort#(add(z0,z1)) -> c_24(f_3#(split(z0,z1),z0,z1),split#(z0,z1)):24 -->_2 qsort#(add(z0,z1)) -> c_24(f_3#(split(z0,z1),z0,z1),split#(z0,z1)):24 -->_4 QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),split#(z0,z1),SPLIT#(z0,z1)):6 -->_3 qsort#(nil()) -> c_25():25 -->_2 qsort#(nil()) -> c_25():25 -->_4 QSORT#(nil()) -> c_12():13 -->_1 APPEND#(nil(),z0) -> c_2():8 -->_1 APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)):1 5:S:LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) -->_1 LT#(s(z0),0()) -> c_9():12 -->_1 LT#(0(),s(z0)) -> c_8():11 -->_1 LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)):5 6:S:QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),split#(z0,z1),SPLIT#(z0,z1)) -->_2 split#(z0,add(z1,z2)) -> c_26(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)):26 -->_3 SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),split#(z0,z2),SPLIT#(z0,z2)):7 -->_2 split#(z0,nil()) -> c_27():27 -->_3 SPLIT#(z0,nil()) -> c_14():14 -->_1 F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))) ,qsort#(z0) ,qsort#(z1) ,QSORT#(z1)):4 -->_1 F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))) ,qsort#(z0) ,qsort#(z1) ,QSORT#(z0)):3 7:S:SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),split#(z0,z2),SPLIT#(z0,z2)) -->_2 split#(z0,add(z1,z2)) -> c_26(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)):26 -->_2 split#(z0,nil()) -> c_27():27 -->_3 SPLIT#(z0,nil()) -> c_14():14 -->_3 SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),split#(z0,z2),SPLIT#(z0,z2)):7 -->_1 F_1#(pair(z0,z1),z2,z3,z4) -> c_3(F_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3),LT#(z2,z3)):2 8:W:APPEND#(nil(),z0) -> c_2() 9:W:F_2#(false(),z0,z1,z2,z3,z4) -> c_4() 10:W:F_2#(true(),z0,z1,z2,z3,z4) -> c_5() 11:W:LT#(0(),s(z0)) -> c_8() 12:W:LT#(s(z0),0()) -> c_9() 13:W:QSORT#(nil()) -> c_12() 14:W:SPLIT#(z0,nil()) -> c_14() 15:W:append#(add(z0,z1),z2) -> c_15(append#(z1,z2)) -->_1 append#(nil(),z0) -> c_16():16 -->_1 append#(add(z0,z1),z2) -> c_15(append#(z1,z2)):15 16:W:append#(nil(),z0) -> c_16() 17:W:f_1#(pair(z0,z1),z2,z3,z4) -> c_17(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) -->_2 lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)):23 -->_2 lt#(s(z0),0()) -> c_22():22 -->_2 lt#(0(),s(z0)) -> c_21():21 -->_1 f_2#(true(),z0,z1,z2,z3,z4) -> c_19():19 -->_1 f_2#(false(),z0,z1,z2,z3,z4) -> c_18():18 18:W:f_2#(false(),z0,z1,z2,z3,z4) -> c_18() 19:W:f_2#(true(),z0,z1,z2,z3,z4) -> c_19() 20:W:f_3#(pair(z0,z1),z2,z3) -> c_20(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) -->_3 qsort#(add(z0,z1)) -> c_24(f_3#(split(z0,z1),z0,z1),split#(z0,z1)):24 -->_2 qsort#(add(z0,z1)) -> c_24(f_3#(split(z0,z1),z0,z1),split#(z0,z1)):24 -->_3 qsort#(nil()) -> c_25():25 -->_2 qsort#(nil()) -> c_25():25 -->_1 append#(nil(),z0) -> c_16():16 -->_1 append#(add(z0,z1),z2) -> c_15(append#(z1,z2)):15 21:W:lt#(0(),s(z0)) -> c_21() 22:W:lt#(s(z0),0()) -> c_22() 23:W:lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)) -->_1 lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)):23 -->_1 lt#(s(z0),0()) -> c_22():22 -->_1 lt#(0(),s(z0)) -> c_21():21 24:W:qsort#(add(z0,z1)) -> c_24(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) -->_2 split#(z0,add(z1,z2)) -> c_26(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)):26 -->_2 split#(z0,nil()) -> c_27():27 -->_1 f_3#(pair(z0,z1),z2,z3) -> c_20(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)):20 25:W:qsort#(nil()) -> c_25() 26:W:split#(z0,add(z1,z2)) -> c_26(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) -->_2 split#(z0,nil()) -> c_27():27 -->_2 split#(z0,add(z1,z2)) -> c_26(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)):26 -->_1 f_1#(pair(z0,z1),z2,z3,z4) -> c_17(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)):17 27:W:split#(z0,nil()) -> c_27() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 13: QSORT#(nil()) -> c_12() 14: SPLIT#(z0,nil()) -> c_14() 24: qsort#(add(z0,z1)) -> c_24(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) 20: f_3#(pair(z0,z1),z2,z3) -> c_20(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) 15: append#(add(z0,z1),z2) -> c_15(append#(z1,z2)) 16: append#(nil(),z0) -> c_16() 25: qsort#(nil()) -> c_25() 26: split#(z0,add(z1,z2)) -> c_26(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) 17: f_1#(pair(z0,z1),z2,z3,z4) -> c_17(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) 18: f_2#(false(),z0,z1,z2,z3,z4) -> c_18() 19: f_2#(true(),z0,z1,z2,z3,z4) -> c_19() 27: split#(z0,nil()) -> c_27() 9: F_2#(false(),z0,z1,z2,z3,z4) -> c_4() 10: F_2#(true(),z0,z1,z2,z3,z4) -> c_5() 11: LT#(0(),s(z0)) -> c_8() 12: LT#(s(z0),0()) -> c_9() 23: lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)) 21: lt#(0(),s(z0)) -> c_21() 22: lt#(s(z0),0()) -> c_22() 8: APPEND#(nil(),z0) -> c_2() ** Step 1.b:4: SimplifyRHS. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) F_1#(pair(z0,z1),z2,z3,z4) -> c_3(F_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3),LT#(z2,z3)) F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1),QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1),QSORT#(z1)) LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),split#(z0,z1),SPLIT#(z0,z1)) SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),split#(z0,z2),SPLIT#(z0,z2)) - Weak TRS: APPEND(add(z0,z1),z2) -> c4(APPEND(z1,z2)) APPEND(nil(),z0) -> c3() F_1(pair(z0,z1),z2,z3,z4) -> c7(F_2(lt(z2,z3),z2,z3,z4,z0,z1),LT(z2,z3)) F_2(false(),z0,z1,z2,z3,z4) -> c9() F_2(true(),z0,z1,z2,z3,z4) -> c8() F_3(pair(z0,z1),z2,z3) -> c12(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z0)) F_3(pair(z0,z1),z2,z3) -> c13(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z1)) LT(0(),s(z0)) -> c() LT(s(z0),0()) -> c1() LT(s(z0),s(z1)) -> c2(LT(z0,z1)) QSORT(add(z0,z1)) -> c11(F_3(split(z0,z1),z0,z1),SPLIT(z0,z1)) QSORT(nil()) -> c10() SPLIT(z0,add(z1,z2)) -> c6(F_1(split(z0,z2),z0,z1,z2),SPLIT(z0,z2)) SPLIT(z0,nil()) -> c5() append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/4,c_7/4,c_8/0,c_9/0,c_10/1,c_11/3,c_12/0,c_13/3,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) -->_1 APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)):1 2:S:F_1#(pair(z0,z1),z2,z3,z4) -> c_3(F_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3),LT#(z2,z3)) -->_3 LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)):5 3:S:F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1),QSORT#(z0)) -->_4 QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),split#(z0,z1),SPLIT#(z0,z1)):6 -->_1 APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)):1 4:S:F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1),QSORT#(z1)) -->_4 QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),split#(z0,z1),SPLIT#(z0,z1)):6 -->_1 APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)):1 5:S:LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) -->_1 LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)):5 6:S:QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),split#(z0,z1),SPLIT#(z0,z1)) -->_3 SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),split#(z0,z2),SPLIT#(z0,z2)):7 -->_1 F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))) ,qsort#(z0) ,qsort#(z1) ,QSORT#(z1)):4 -->_1 F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))) ,qsort#(z0) ,qsort#(z1) ,QSORT#(z0)):3 7:S:SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),split#(z0,z2),SPLIT#(z0,z2)) -->_3 SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),split#(z0,z2),SPLIT#(z0,z2)):7 -->_1 F_1#(pair(z0,z1),z2,z3,z4) -> c_3(F_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3),LT#(z2,z3)):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: F_1#(pair(z0,z1),z2,z3,z4) -> c_3(LT#(z2,z3)) F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z1)) QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),SPLIT#(z0,z1)) SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),SPLIT#(z0,z2)) ** Step 1.b:5: UsableRules. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) F_1#(pair(z0,z1),z2,z3,z4) -> c_3(LT#(z2,z3)) F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z1)) LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),SPLIT#(z0,z1)) SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),SPLIT#(z0,z2)) - Weak TRS: APPEND(add(z0,z1),z2) -> c4(APPEND(z1,z2)) APPEND(nil(),z0) -> c3() F_1(pair(z0,z1),z2,z3,z4) -> c7(F_2(lt(z2,z3),z2,z3,z4,z0,z1),LT(z2,z3)) F_2(false(),z0,z1,z2,z3,z4) -> c9() F_2(true(),z0,z1,z2,z3,z4) -> c8() F_3(pair(z0,z1),z2,z3) -> c12(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z0)) F_3(pair(z0,z1),z2,z3) -> c13(APPEND(qsort(z0),add(z3,qsort(z1))),QSORT(z1)) LT(0(),s(z0)) -> c() LT(s(z0),0()) -> c1() LT(s(z0),s(z1)) -> c2(LT(z0,z1)) QSORT(add(z0,z1)) -> c11(F_3(split(z0,z1),z0,z1),SPLIT(z0,z1)) QSORT(nil()) -> c10() SPLIT(z0,add(z1,z2)) -> c6(F_1(split(z0,z2),z0,z1,z2),SPLIT(z0,z2)) SPLIT(z0,nil()) -> c5() append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) F_1#(pair(z0,z1),z2,z3,z4) -> c_3(LT#(z2,z3)) F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z1)) LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),SPLIT#(z0,z1)) SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),SPLIT#(z0,z2)) ** Step 1.b:6: DecomposeDG. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) F_1#(pair(z0,z1),z2,z3,z4) -> c_3(LT#(z2,z3)) F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z1)) LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),SPLIT#(z0,z1)) SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),SPLIT#(z0,z2)) - Weak TRS: append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + 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 F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z1)) QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),SPLIT#(z0,z1)) and a lower component APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) F_1#(pair(z0,z1),z2,z3,z4) -> c_3(LT#(z2,z3)) LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),SPLIT#(z0,z2)) Further, following extension rules are added to the lower component. F_3#(pair(z0,z1),z2,z3) -> APPEND#(qsort(z0),add(z3,qsort(z1))) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) *** Step 1.b:6.a:1: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z1)) QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),SPLIT#(z0,z1)) - Weak TRS: append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z0)) -->_2 QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),SPLIT#(z0,z1)):3 2:S:F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z1)) -->_2 QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),SPLIT#(z0,z1)):3 3:S:QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1),SPLIT#(z0,z1)) -->_1 F_3#(pair(z0,z1),z2,z3) -> c_7(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z1)):2 -->_1 F_3#(pair(z0,z1),z2,z3) -> c_6(APPEND#(qsort(z0),add(z3,qsort(z1))),QSORT#(z0)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: F_3#(pair(z0,z1),z2,z3) -> c_6(QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(QSORT#(z1)) QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1)) *** Step 1.b:6.a:2: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: F_3#(pair(z0,z1),z2,z3) -> c_6(QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(QSORT#(z1)) QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1)) - Weak TRS: append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/2,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) F_3#(pair(z0,z1),z2,z3) -> c_6(QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(QSORT#(z1)) QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1)) *** Step 1.b:6.a:3: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: F_3#(pair(z0,z1),z2,z3) -> c_6(QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(QSORT#(z1)) QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1)) - Weak TRS: f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/2,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + 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_6) = {1}, uargs(c_7) = {1}, uargs(c_11) = {1} Following symbols are considered usable: {f_1,f_2,lt,split,APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1#,f_2#,f_3#,lt#,qsort#,split#} TcT has computed the following interpretation: p(0) = [8] p(APPEND) = [1] x2 + [8] p(F_1) = [1] x1 + [2] x2 + [2] x3 + [8] x4 + [0] p(F_2) = [1] x1 + [2] x3 + [2] x4 + [1] x5 + [1] x6 + [0] p(F_3) = [1] x1 + [1] x2 + [8] p(LT) = [1] x1 + [1] p(QSORT) = [2] x1 + [1] p(SPLIT) = [2] x1 + [2] x2 + [2] p(add) = [1] x1 + [1] x2 + [4] p(append) = [1] x1 + [1] x2 + [1] p(c) = [1] p(c1) = [1] p(c10) = [1] p(c11) = [2] p(c12) = [1] x1 + [1] x2 + [1] p(c13) = [1] x1 + [2] p(c2) = [2] p(c3) = [2] p(c4) = [1] p(c5) = [2] p(c6) = [1] x1 + [1] p(c7) = [1] x1 + [1] p(c8) = [1] p(c9) = [0] p(f_1) = [1] x1 + [1] x3 + [4] p(f_2) = [4] x1 + [1] x3 + [1] x5 + [1] x6 + [0] p(f_3) = [1] x1 + [8] x3 + [1] p(false) = [1] p(lt) = [1] p(nil) = [0] p(pair) = [1] x1 + [1] x2 + [0] p(qsort) = [1] x1 + [8] p(s) = [1] x1 + [4] p(split) = [1] x2 + [0] p(true) = [1] p(APPEND#) = [2] x1 + [1] x2 + [1] p(F_1#) = [1] x1 + [8] x2 + [1] x3 + [2] x4 + [0] p(F_2#) = [2] x3 + [1] x6 + [1] p(F_3#) = [1] x1 + [0] p(LT#) = [0] p(QSORT#) = [1] x1 + [0] p(SPLIT#) = [1] x1 + [1] p(append#) = [1] x1 + [1] x2 + [2] p(f_1#) = [1] x1 + [4] x2 + [1] x3 + [1] p(f_2#) = [1] x1 + [2] x4 + [2] x5 + [1] x6 + [0] p(f_3#) = [1] x2 + [1] x3 + [1] p(lt#) = [2] x1 + [1] x2 + [8] p(qsort#) = [1] x1 + [4] p(split#) = [1] x1 + [1] x2 + [1] p(c_1) = [1] x1 + [2] p(c_2) = [1] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [8] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [0] p(c_8) = [2] p(c_9) = [0] p(c_10) = [1] x1 + [2] p(c_11) = [1] x1 + [0] p(c_12) = [2] p(c_13) = [1] x2 + [0] p(c_14) = [2] p(c_15) = [2] p(c_16) = [2] p(c_17) = [1] x2 + [0] p(c_18) = [1] p(c_19) = [0] p(c_20) = [1] x1 + [8] x3 + [1] p(c_21) = [2] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [2] p(c_26) = [1] x1 + [1] x2 + [2] p(c_27) = [0] Following rules are strictly oriented: QSORT#(add(z0,z1)) = [1] z0 + [1] z1 + [4] > [1] z1 + [0] = c_11(F_3#(split(z0,z1),z0,z1)) Following rules are (at-least) weakly oriented: F_3#(pair(z0,z1),z2,z3) = [1] z0 + [1] z1 + [0] >= [1] z0 + [0] = c_6(QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) = [1] z0 + [1] z1 + [0] >= [1] z1 + [0] = c_7(QSORT#(z1)) f_1(pair(z0,z1),z2,z3,z4) = [1] z0 + [1] z1 + [1] z3 + [4] >= [1] z0 + [1] z1 + [1] z3 + [4] = f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) = [1] z1 + [1] z3 + [1] z4 + [4] >= [1] z1 + [1] z3 + [1] z4 + [4] = pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) = [1] z1 + [1] z3 + [1] z4 + [4] >= [1] z1 + [1] z3 + [1] z4 + [4] = pair(z3,add(z1,z4)) lt(0(),s(z0)) = [1] >= [1] = true() lt(s(z0),0()) = [1] >= [1] = false() lt(s(z0),s(z1)) = [1] >= [1] = lt(z0,z1) split(z0,add(z1,z2)) = [1] z1 + [1] z2 + [4] >= [1] z1 + [1] z2 + [4] = f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) = [0] >= [0] = pair(nil(),nil()) *** Step 1.b:6.a:4: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: F_3#(pair(z0,z1),z2,z3) -> c_6(QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(QSORT#(z1)) - Weak DPs: QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1)) - Weak TRS: f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/2,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + 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_6) = {1}, uargs(c_7) = {1}, uargs(c_11) = {1} Following symbols are considered usable: {f_1,f_2,lt,split,APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1#,f_2#,f_3#,lt#,qsort#,split#} TcT has computed the following interpretation: p(0) = [0] p(APPEND) = [1] x2 + [1] p(F_1) = [8] x1 + [1] p(F_2) = [2] x2 + [2] x4 + [1] x5 + [2] x6 + [1] p(F_3) = [1] x1 + [1] x3 + [2] p(LT) = [8] p(QSORT) = [2] p(SPLIT) = [1] x2 + [0] p(add) = [1] x2 + [15] p(append) = [1] x1 + [1] p(c) = [1] p(c1) = [1] p(c10) = [0] p(c11) = [0] p(c12) = [1] x1 + [1] x2 + [4] p(c13) = [1] x1 + [1] p(c2) = [1] p(c3) = [2] p(c4) = [8] p(c5) = [1] p(c6) = [1] x1 + [1] x2 + [0] p(c7) = [0] p(c8) = [2] p(c9) = [2] p(f_1) = [1] x1 + [15] p(f_2) = [6] x1 + [1] x5 + [1] x6 + [0] p(f_3) = [1] x1 + [0] p(false) = [3] p(lt) = [3] p(nil) = [0] p(pair) = [1] x1 + [1] x2 + [3] p(qsort) = [1] p(s) = [1] x1 + [0] p(split) = [1] x2 + [3] p(true) = [3] p(APPEND#) = [2] x1 + [2] p(F_1#) = [1] x1 + [0] p(F_2#) = [2] x1 + [1] x2 + [1] x3 + [2] x5 + [1] x6 + [1] p(F_3#) = [2] x1 + [0] p(LT#) = [1] x1 + [1] x2 + [8] p(QSORT#) = [2] x1 + [1] p(SPLIT#) = [0] p(append#) = [1] x1 + [1] x2 + [8] p(f_1#) = [1] x1 + [1] x2 + [2] x3 + [4] p(f_2#) = [1] x1 + [1] x2 + [1] x5 + [1] x6 + [0] p(f_3#) = [1] x2 + [2] x3 + [1] p(lt#) = [1] x1 + [1] p(qsort#) = [0] p(split#) = [1] x2 + [0] p(c_1) = [1] x1 + [1] p(c_2) = [0] p(c_3) = [2] x1 + [1] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [4] p(c_7) = [1] x1 + [0] p(c_8) = [1] p(c_9) = [0] p(c_10) = [2] p(c_11) = [1] x1 + [12] p(c_12) = [1] p(c_13) = [1] x1 + [1] x2 + [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [2] p(c_18) = [1] p(c_19) = [1] p(c_20) = [4] x1 + [1] x2 + [1] x3 + [1] p(c_21) = [1] p(c_22) = [1] p(c_23) = [0] p(c_24) = [1] x2 + [1] p(c_25) = [1] p(c_26) = [1] p(c_27) = [0] Following rules are strictly oriented: F_3#(pair(z0,z1),z2,z3) = [2] z0 + [2] z1 + [6] > [2] z0 + [5] = c_6(QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) = [2] z0 + [2] z1 + [6] > [2] z1 + [1] = c_7(QSORT#(z1)) Following rules are (at-least) weakly oriented: QSORT#(add(z0,z1)) = [2] z1 + [31] >= [2] z1 + [18] = c_11(F_3#(split(z0,z1),z0,z1)) f_1(pair(z0,z1),z2,z3,z4) = [1] z0 + [1] z1 + [18] >= [1] z0 + [1] z1 + [18] = f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) = [1] z3 + [1] z4 + [18] >= [1] z3 + [1] z4 + [18] = pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) = [1] z3 + [1] z4 + [18] >= [1] z3 + [1] z4 + [18] = pair(z3,add(z1,z4)) lt(0(),s(z0)) = [3] >= [3] = true() lt(s(z0),0()) = [3] >= [3] = false() lt(s(z0),s(z1)) = [3] >= [3] = lt(z0,z1) split(z0,add(z1,z2)) = [1] z2 + [18] >= [1] z2 + [18] = f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) = [3] >= [3] = pair(nil(),nil()) *** Step 1.b:6.a:5: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: F_3#(pair(z0,z1),z2,z3) -> c_6(QSORT#(z0)) F_3#(pair(z0,z1),z2,z3) -> c_7(QSORT#(z1)) QSORT#(add(z0,z1)) -> c_11(F_3#(split(z0,z1),z0,z1)) - Weak TRS: f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/2,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 1.b:6.b:1: DecomposeDG. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) F_1#(pair(z0,z1),z2,z3,z4) -> c_3(LT#(z2,z3)) LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),SPLIT#(z0,z2)) - Weak DPs: F_3#(pair(z0,z1),z2,z3) -> APPEND#(qsort(z0),add(z3,qsort(z1))) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) - Weak TRS: append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + 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 APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) F_3#(pair(z0,z1),z2,z3) -> APPEND#(qsort(z0),add(z3,qsort(z1))) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),SPLIT#(z0,z2)) and a lower component F_1#(pair(z0,z1),z2,z3,z4) -> c_3(LT#(z2,z3)) LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) Further, following extension rules are added to the lower component. APPEND#(add(z0,z1),z2) -> APPEND#(z1,z2) F_3#(pair(z0,z1),z2,z3) -> APPEND#(qsort(z0),add(z3,qsort(z1))) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) SPLIT#(z0,add(z1,z2)) -> F_1#(split(z0,z2),z0,z1,z2) SPLIT#(z0,add(z1,z2)) -> SPLIT#(z0,z2) **** Step 1.b:6.b:1.a:1: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),SPLIT#(z0,z2)) - Weak DPs: F_3#(pair(z0,z1),z2,z3) -> APPEND#(qsort(z0),add(z3,qsort(z1))) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) - Weak TRS: append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) -->_1 APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)):1 2:S:SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),SPLIT#(z0,z2)) -->_2 SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),SPLIT#(z0,z2)):2 3:W:F_3#(pair(z0,z1),z2,z3) -> APPEND#(qsort(z0),add(z3,qsort(z1))) -->_1 APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)):1 4:W:F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) -->_1 QSORT#(add(z0,z1)) -> SPLIT#(z0,z1):7 -->_1 QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1):6 5:W:F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) -->_1 QSORT#(add(z0,z1)) -> SPLIT#(z0,z1):7 -->_1 QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1):6 6:W:QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) -->_1 F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1):5 -->_1 F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0):4 -->_1 F_3#(pair(z0,z1),z2,z3) -> APPEND#(qsort(z0),add(z3,qsort(z1))):3 7:W:QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) -->_1 SPLIT#(z0,add(z1,z2)) -> c_13(F_1#(split(z0,z2),z0,z1,z2),SPLIT#(z0,z2)):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: SPLIT#(z0,add(z1,z2)) -> c_13(SPLIT#(z0,z2)) **** Step 1.b:6.b:1.a:2: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) SPLIT#(z0,add(z1,z2)) -> c_13(SPLIT#(z0,z2)) - Weak DPs: F_3#(pair(z0,z1),z2,z3) -> APPEND#(qsort(z0),add(z3,qsort(z1))) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) - Weak TRS: append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + 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_13) = {1} Following symbols are considered usable: {f_1,f_2,split,APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1#,f_2#,f_3#,lt#,qsort#,split#} TcT has computed the following interpretation: p(0) = [1] p(APPEND) = [1] p(F_1) = [1] x2 + [1] x3 + [4] x4 + [0] p(F_2) = [2] x1 + [1] x3 + [1] p(F_3) = [1] x1 + [1] x2 + [1] x3 + [4] p(LT) = [4] x2 + [1] p(QSORT) = [1] p(SPLIT) = [2] x1 + [2] p(add) = [1] x2 + [1] p(append) = [4] x2 + [3] p(c) = [4] p(c1) = [0] p(c10) = [0] p(c11) = [1] x1 + [1] p(c12) = [4] p(c13) = [4] p(c2) = [1] x1 + [0] p(c3) = [1] p(c4) = [1] x1 + [0] p(c5) = [0] p(c6) = [1] x2 + [1] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(f_1) = [1] x1 + [1] p(f_2) = [1] x5 + [1] x6 + [1] p(f_3) = [4] x1 + [4] x2 + [7] x3 + [0] p(false) = [0] p(lt) = [0] p(nil) = [0] p(pair) = [1] x1 + [1] x2 + [0] p(qsort) = [1] x1 + [2] p(s) = [1] p(split) = [1] x2 + [0] p(true) = [0] p(APPEND#) = [0] p(F_1#) = [4] x2 + [1] x3 + [1] x4 + [1] p(F_2#) = [4] x5 + [1] p(F_3#) = [1] x1 + [3] p(LT#) = [1] x1 + [1] x2 + [1] p(QSORT#) = [1] x1 + [3] p(SPLIT#) = [1] x2 + [0] p(append#) = [1] x2 + [1] p(f_1#) = [1] p(f_2#) = [1] x2 + [1] x4 + [0] p(f_3#) = [2] p(lt#) = [4] p(qsort#) = [1] x1 + [0] p(split#) = [1] p(c_1) = [4] x1 + [0] p(c_2) = [4] p(c_3) = [4] p(c_4) = [1] p(c_5) = [2] p(c_6) = [4] x2 + [0] p(c_7) = [1] x1 + [1] x2 + [2] p(c_8) = [4] p(c_9) = [0] p(c_10) = [2] p(c_11) = [1] x1 + [1] x2 + [1] p(c_12) = [1] p(c_13) = [1] x1 + [0] p(c_14) = [1] p(c_15) = [2] x1 + [1] p(c_16) = [2] p(c_17) = [1] x1 + [0] p(c_18) = [1] p(c_19) = [2] p(c_20) = [1] x1 + [0] p(c_21) = [0] p(c_22) = [4] p(c_23) = [0] p(c_24) = [1] x2 + [0] p(c_25) = [2] p(c_26) = [4] x1 + [1] p(c_27) = [1] Following rules are strictly oriented: SPLIT#(z0,add(z1,z2)) = [1] z2 + [1] > [1] z2 + [0] = c_13(SPLIT#(z0,z2)) Following rules are (at-least) weakly oriented: APPEND#(add(z0,z1),z2) = [0] >= [0] = c_1(APPEND#(z1,z2)) F_3#(pair(z0,z1),z2,z3) = [1] z0 + [1] z1 + [3] >= [0] = APPEND#(qsort(z0),add(z3,qsort(z1))) F_3#(pair(z0,z1),z2,z3) = [1] z0 + [1] z1 + [3] >= [1] z0 + [3] = QSORT#(z0) F_3#(pair(z0,z1),z2,z3) = [1] z0 + [1] z1 + [3] >= [1] z1 + [3] = QSORT#(z1) QSORT#(add(z0,z1)) = [1] z1 + [4] >= [1] z1 + [3] = F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) = [1] z1 + [4] >= [1] z1 + [0] = SPLIT#(z0,z1) f_1(pair(z0,z1),z2,z3,z4) = [1] z0 + [1] z1 + [1] >= [1] z0 + [1] z1 + [1] = f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) = [1] z3 + [1] z4 + [1] >= [1] z3 + [1] z4 + [1] = pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) = [1] z3 + [1] z4 + [1] >= [1] z3 + [1] z4 + [1] = pair(z3,add(z1,z4)) split(z0,add(z1,z2)) = [1] z2 + [1] >= [1] z2 + [1] = f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) = [0] >= [0] = pair(nil(),nil()) **** Step 1.b:6.b:1.a:3: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) - Weak DPs: F_3#(pair(z0,z1),z2,z3) -> APPEND#(qsort(z0),add(z3,qsort(z1))) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) SPLIT#(z0,add(z1,z2)) -> c_13(SPLIT#(z0,z2)) - Weak TRS: append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + 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(add) = {2}, uargs(append) = {1,2}, uargs(f_1) = {1}, uargs(f_2) = {1}, uargs(f_3) = {1}, uargs(APPEND#) = {1,2}, uargs(F_3#) = {1}, uargs(c_1) = {1}, uargs(c_13) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(APPEND) = [0] p(F_1) = [0] p(F_2) = [0] p(F_3) = [0] p(LT) = [0] p(QSORT) = [4] x1 + [0] p(SPLIT) = [1] x2 + [2] p(add) = [1] x2 + [1] p(append) = [1] x1 + [1] x2 + [0] p(c) = [0] p(c1) = [0] p(c10) = [4] p(c11) = [1] x1 + [1] x2 + [2] p(c12) = [1] p(c13) = [1] x1 + [1] x2 + [1] p(c2) = [2] p(c3) = [0] p(c4) = [4] p(c5) = [0] p(c6) = [0] p(c7) = [1] p(c8) = [0] p(c9) = [1] p(f_1) = [1] x1 + [1] p(f_2) = [1] x1 + [1] x5 + [1] x6 + [0] p(f_3) = [1] x1 + [1] p(false) = [1] tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list p(lt) = [1] p(nil) = [0] p(pair) = [1] x1 + [1] x2 + [0] p(qsort) = [1] x1 + [0] p(s) = [0] p(split) = [1] x2 + [0] p(true) = [1] p(APPEND#) = [1] x1 + [1] x2 + [0] p(F_1#) = [1] x2 + [1] x3 + [2] p(F_2#) = [2] x1 + [1] x2 + [1] x3 + [1] x4 + [1] x6 + [2] p(F_3#) = [1] x1 + [2] p(LT#) = [0] p(QSORT#) = [1] x1 + [2] p(SPLIT#) = [0] p(append#) = [1] x1 + [4] x2 + [4] p(f_1#) = [0] p(f_2#) = [1] x1 + [1] x2 + [1] x3 + [2] x4 + [1] x6 + [4] p(f_3#) = [1] x1 + [0] p(lt#) = [1] x1 + [1] p(qsort#) = [1] p(split#) = [1] x2 + [0] p(c_1) = [1] x1 + [0] p(c_2) = [2] p(c_3) = [1] x1 + [0] p(c_4) = [1] p(c_5) = [0] p(c_6) = [1] x1 + [1] x2 + [1] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [0] p(c_9) = [4] p(c_10) = [1] x1 + [0] p(c_11) = [1] x2 + [1] p(c_12) = [0] p(c_13) = [1] x1 + [0] p(c_14) = [2] p(c_15) = [4] x1 + [4] p(c_16) = [2] p(c_17) = [1] x1 + [1] p(c_18) = [0] p(c_19) = [0] p(c_20) = [1] x2 + [2] x3 + [1] p(c_21) = [2] p(c_22) = [0] p(c_23) = [0] p(c_24) = [2] x2 + [0] p(c_25) = [2] p(c_26) = [1] x2 + [2] p(c_27) = [0] Following rules are strictly oriented: APPEND#(add(z0,z1),z2) = [1] z1 + [1] z2 + [1] > [1] z1 + [1] z2 + [0] = c_1(APPEND#(z1,z2)) Following rules are (at-least) weakly oriented: F_3#(pair(z0,z1),z2,z3) = [1] z0 + [1] z1 + [2] >= [1] z0 + [1] z1 + [1] = APPEND#(qsort(z0),add(z3,qsort(z1))) F_3#(pair(z0,z1),z2,z3) = [1] z0 + [1] z1 + [2] >= [1] z0 + [2] = QSORT#(z0) F_3#(pair(z0,z1),z2,z3) = [1] z0 + [1] z1 + [2] >= [1] z1 + [2] = QSORT#(z1) QSORT#(add(z0,z1)) = [1] z1 + [3] >= [1] z1 + [2] = F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) = [1] z1 + [3] >= [0] = SPLIT#(z0,z1) SPLIT#(z0,add(z1,z2)) = [0] >= [0] = c_13(SPLIT#(z0,z2)) append(add(z0,z1),z2) = [1] z1 + [1] z2 + [1] >= [1] z1 + [1] z2 + [1] = add(z0,append(z1,z2)) append(nil(),z0) = [1] z0 + [0] >= [1] z0 + [0] = z0 f_1(pair(z0,z1),z2,z3,z4) = [1] z0 + [1] z1 + [1] >= [1] z0 + [1] z1 + [1] = f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) = [1] z3 + [1] z4 + [1] >= [1] z3 + [1] z4 + [1] = pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) = [1] z3 + [1] z4 + [1] >= [1] z3 + [1] z4 + [1] = pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) = [1] z0 + [1] z1 + [1] >= [1] z0 + [1] z1 + [1] = append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) = [1] >= [1] = true() lt(s(z0),0()) = [1] >= [1] = false() lt(s(z0),s(z1)) = [1] >= [1] = lt(z0,z1) qsort(add(z0,z1)) = [1] z1 + [1] >= [1] z1 + [1] = f_3(split(z0,z1),z0,z1) qsort(nil()) = [0] >= [0] = nil() split(z0,add(z1,z2)) = [1] z2 + [1] >= [1] z2 + [1] = f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) = [0] >= [0] = pair(nil(),nil()) Further, it can be verified that all rules not oriented are covered by the weightgap condition. **** Step 1.b:6.b:1.a:4: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: APPEND#(add(z0,z1),z2) -> c_1(APPEND#(z1,z2)) F_3#(pair(z0,z1),z2,z3) -> APPEND#(qsort(z0),add(z3,qsort(z1))) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) SPLIT#(z0,add(z1,z2)) -> c_13(SPLIT#(z0,z2)) - Weak TRS: append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). **** Step 1.b:6.b:1.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: F_1#(pair(z0,z1),z2,z3,z4) -> c_3(LT#(z2,z3)) LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) - Weak DPs: APPEND#(add(z0,z1),z2) -> APPEND#(z1,z2) F_3#(pair(z0,z1),z2,z3) -> APPEND#(qsort(z0),add(z3,qsort(z1))) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) SPLIT#(z0,add(z1,z2)) -> F_1#(split(z0,z2),z0,z1,z2) SPLIT#(z0,add(z1,z2)) -> SPLIT#(z0,z2) - Weak TRS: append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:F_1#(pair(z0,z1),z2,z3,z4) -> c_3(LT#(z2,z3)) -->_1 LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)):2 2:S:LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) -->_1 LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)):2 3:W:APPEND#(add(z0,z1),z2) -> APPEND#(z1,z2) -->_1 APPEND#(add(z0,z1),z2) -> APPEND#(z1,z2):3 4:W:F_3#(pair(z0,z1),z2,z3) -> APPEND#(qsort(z0),add(z3,qsort(z1))) -->_1 APPEND#(add(z0,z1),z2) -> APPEND#(z1,z2):3 5:W:F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) -->_1 QSORT#(add(z0,z1)) -> SPLIT#(z0,z1):8 -->_1 QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1):7 6:W:F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) -->_1 QSORT#(add(z0,z1)) -> SPLIT#(z0,z1):8 -->_1 QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1):7 7:W:QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) -->_1 F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1):6 -->_1 F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0):5 -->_1 F_3#(pair(z0,z1),z2,z3) -> APPEND#(qsort(z0),add(z3,qsort(z1))):4 8:W:QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) -->_1 SPLIT#(z0,add(z1,z2)) -> SPLIT#(z0,z2):10 -->_1 SPLIT#(z0,add(z1,z2)) -> F_1#(split(z0,z2),z0,z1,z2):9 9:W:SPLIT#(z0,add(z1,z2)) -> F_1#(split(z0,z2),z0,z1,z2) -->_1 F_1#(pair(z0,z1),z2,z3,z4) -> c_3(LT#(z2,z3)):1 10:W:SPLIT#(z0,add(z1,z2)) -> SPLIT#(z0,z2) -->_1 SPLIT#(z0,add(z1,z2)) -> SPLIT#(z0,z2):10 -->_1 SPLIT#(z0,add(z1,z2)) -> F_1#(split(z0,z2),z0,z1,z2):9 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: F_3#(pair(z0,z1),z2,z3) -> APPEND#(qsort(z0),add(z3,qsort(z1))) 3: APPEND#(add(z0,z1),z2) -> APPEND#(z1,z2) **** Step 1.b:6.b:1.b:2: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: F_1#(pair(z0,z1),z2,z3,z4) -> c_3(LT#(z2,z3)) LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) - Weak DPs: F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) SPLIT#(z0,add(z1,z2)) -> F_1#(split(z0,z2),z0,z1,z2) SPLIT#(z0,add(z1,z2)) -> SPLIT#(z0,z2) - Weak TRS: append(add(z0,z1),z2) -> add(z0,append(z1,z2)) append(nil(),z0) -> z0 f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) f_3(pair(z0,z1),z2,z3) -> append(qsort(z0),add(z3,qsort(z1))) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) qsort(add(z0,z1)) -> f_3(split(z0,z1),z0,z1) qsort(nil()) -> nil() split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) F_1#(pair(z0,z1),z2,z3,z4) -> c_3(LT#(z2,z3)) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) SPLIT#(z0,add(z1,z2)) -> F_1#(split(z0,z2),z0,z1,z2) SPLIT#(z0,add(z1,z2)) -> SPLIT#(z0,z2) **** Step 1.b:6.b:1.b:3: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: F_1#(pair(z0,z1),z2,z3,z4) -> c_3(LT#(z2,z3)) LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) - Weak DPs: F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) SPLIT#(z0,add(z1,z2)) -> F_1#(split(z0,z2),z0,z1,z2) SPLIT#(z0,add(z1,z2)) -> SPLIT#(z0,z2) - Weak TRS: f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + 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_3) = {1}, uargs(c_10) = {1} Following symbols are considered usable: {f_1,f_2,lt,split,APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1#,f_2#,f_3#,lt#,qsort#,split#} TcT has computed the following interpretation: p(0) = [0] p(APPEND) = [0] p(F_1) = [0] p(F_2) = [0] p(F_3) = [0] p(LT) = [0] p(QSORT) = [0] p(SPLIT) = [0] p(add) = [0] p(append) = [0] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [0] p(c13) = [0] p(c2) = [0] p(c3) = [0] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(f_1) = [1] p(f_2) = [1] x1 + [0] p(f_3) = [0] p(false) = [1] p(lt) = [1] p(nil) = [0] p(pair) = [1] p(qsort) = [0] p(s) = [0] p(split) = [1] p(true) = [1] p(APPEND#) = [0] p(F_1#) = [5] p(F_2#) = [0] p(F_3#) = [2] x1 + [3] p(LT#) = [3] p(QSORT#) = [5] p(SPLIT#) = [5] p(append#) = [0] p(f_1#) = [0] p(f_2#) = [0] p(f_3#) = [0] p(lt#) = [0] p(qsort#) = [0] p(split#) = [0] p(c_1) = [0] p(c_2) = [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) = [0] p(c_13) = [0] p(c_14) = [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] Following rules are strictly oriented: F_1#(pair(z0,z1),z2,z3,z4) = [5] > [3] = c_3(LT#(z2,z3)) Following rules are (at-least) weakly oriented: F_3#(pair(z0,z1),z2,z3) = [5] >= [5] = QSORT#(z0) F_3#(pair(z0,z1),z2,z3) = [5] >= [5] = QSORT#(z1) LT#(s(z0),s(z1)) = [3] >= [3] = c_10(LT#(z0,z1)) QSORT#(add(z0,z1)) = [5] >= [5] = F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) = [5] >= [5] = SPLIT#(z0,z1) SPLIT#(z0,add(z1,z2)) = [5] >= [5] = F_1#(split(z0,z2),z0,z1,z2) SPLIT#(z0,add(z1,z2)) = [5] >= [5] = SPLIT#(z0,z2) f_1(pair(z0,z1),z2,z3,z4) = [1] >= [1] = f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) = [1] >= [1] = pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) = [1] >= [1] = pair(z3,add(z1,z4)) lt(0(),s(z0)) = [1] >= [1] = true() lt(s(z0),0()) = [1] >= [1] = false() lt(s(z0),s(z1)) = [1] >= [1] = lt(z0,z1) split(z0,add(z1,z2)) = [1] >= [1] = f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) = [1] >= [1] = pair(nil(),nil()) **** Step 1.b:6.b:1.b:4: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) - Weak DPs: F_1#(pair(z0,z1),z2,z3,z4) -> c_3(LT#(z2,z3)) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) SPLIT#(z0,add(z1,z2)) -> F_1#(split(z0,z2),z0,z1,z2) SPLIT#(z0,add(z1,z2)) -> SPLIT#(z0,z2) - Weak TRS: f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + 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_3) = {1}, uargs(c_10) = {1} Following symbols are considered usable: {f_1,f_2,split,APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1#,f_2#,f_3#,lt#,qsort#,split#} TcT has computed the following interpretation: p(0) = [3] p(APPEND) = [4] x2 + [2] p(F_1) = [2] x2 + [1] x3 + [1] x4 + [1] p(F_2) = [1] x1 + [1] x2 + [2] x3 + [1] x4 + [2] p(F_3) = [1] x2 + [2] x3 + [0] p(LT) = [2] x1 + [0] p(QSORT) = [1] p(SPLIT) = [1] x2 + [1] p(add) = [1] x1 + [1] x2 + [0] p(append) = [1] p(c) = [0] p(c1) = [1] p(c10) = [0] p(c11) = [0] p(c12) = [1] x2 + [0] p(c13) = [1] x2 + [0] p(c2) = [1] x1 + [1] p(c3) = [2] p(c4) = [1] p(c5) = [1] p(c6) = [1] p(c7) = [1] p(c8) = [4] p(c9) = [0] p(f_1) = [1] x1 + [1] x3 + [0] p(f_2) = [1] x3 + [1] x5 + [1] x6 + [0] p(f_3) = [1] x2 + [4] p(false) = [4] p(lt) = [4] x1 + [0] p(nil) = [0] p(pair) = [1] x1 + [1] x2 + [0] p(qsort) = [0] p(s) = [1] x1 + [1] p(split) = [1] x2 + [0] p(true) = [0] p(APPEND#) = [1] x1 + [0] p(F_1#) = [1] x3 + [1] x4 + [0] p(F_2#) = [4] x1 + [1] x4 + [1] x6 + [0] p(F_3#) = [1] x1 + [1] x2 + [0] p(LT#) = [1] x2 + [0] p(QSORT#) = [1] x1 + [0] p(SPLIT#) = [1] x2 + [0] p(append#) = [1] x2 + [1] p(f_1#) = [1] x1 + [1] x2 + [1] x4 + [1] p(f_2#) = [1] x3 + [4] x4 + [1] x5 + [1] p(f_3#) = [1] x1 + [4] x3 + [0] p(lt#) = [2] x1 + [0] p(qsort#) = [1] p(split#) = [2] x1 + [0] p(c_1) = [1] x1 + [1] p(c_2) = [1] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [4] p(c_6) = [1] p(c_7) = [2] x2 + [1] p(c_8) = [1] p(c_9) = [2] p(c_10) = [1] x1 + [0] p(c_11) = [4] x1 + [4] x2 + [0] p(c_12) = [0] p(c_13) = [1] x1 + [4] x2 + [2] p(c_14) = [1] p(c_15) = [0] p(c_16) = [0] p(c_17) = [1] p(c_18) = [0] p(c_19) = [0] p(c_20) = [2] p(c_21) = [1] p(c_22) = [1] p(c_23) = [1] x1 + [0] p(c_24) = [1] x1 + [1] x2 + [0] p(c_25) = [1] p(c_26) = [2] x2 + [0] p(c_27) = [0] Following rules are strictly oriented: LT#(s(z0),s(z1)) = [1] z1 + [1] > [1] z1 + [0] = c_10(LT#(z0,z1)) Following rules are (at-least) weakly oriented: F_1#(pair(z0,z1),z2,z3,z4) = [1] z3 + [1] z4 + [0] >= [1] z3 + [0] = c_3(LT#(z2,z3)) F_3#(pair(z0,z1),z2,z3) = [1] z0 + [1] z1 + [1] z2 + [0] >= [1] z0 + [0] = QSORT#(z0) F_3#(pair(z0,z1),z2,z3) = [1] z0 + [1] z1 + [1] z2 + [0] >= [1] z1 + [0] = QSORT#(z1) QSORT#(add(z0,z1)) = [1] z0 + [1] z1 + [0] >= [1] z0 + [1] z1 + [0] = F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) = [1] z0 + [1] z1 + [0] >= [1] z1 + [0] = SPLIT#(z0,z1) SPLIT#(z0,add(z1,z2)) = [1] z1 + [1] z2 + [0] >= [1] z1 + [1] z2 + [0] = F_1#(split(z0,z2),z0,z1,z2) SPLIT#(z0,add(z1,z2)) = [1] z1 + [1] z2 + [0] >= [1] z2 + [0] = SPLIT#(z0,z2) f_1(pair(z0,z1),z2,z3,z4) = [1] z0 + [1] z1 + [1] z3 + [0] >= [1] z0 + [1] z1 + [1] z3 + [0] = f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) = [1] z1 + [1] z3 + [1] z4 + [0] >= [1] z1 + [1] z3 + [1] z4 + [0] = pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) = [1] z1 + [1] z3 + [1] z4 + [0] >= [1] z1 + [1] z3 + [1] z4 + [0] = pair(z3,add(z1,z4)) split(z0,add(z1,z2)) = [1] z1 + [1] z2 + [0] >= [1] z1 + [1] z2 + [0] = f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) = [0] >= [0] = pair(nil(),nil()) **** Step 1.b:6.b:1.b:5: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: F_1#(pair(z0,z1),z2,z3,z4) -> c_3(LT#(z2,z3)) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z0) F_3#(pair(z0,z1),z2,z3) -> QSORT#(z1) LT#(s(z0),s(z1)) -> c_10(LT#(z0,z1)) QSORT#(add(z0,z1)) -> F_3#(split(z0,z1),z0,z1) QSORT#(add(z0,z1)) -> SPLIT#(z0,z1) SPLIT#(z0,add(z1,z2)) -> F_1#(split(z0,z2),z0,z1,z2) SPLIT#(z0,add(z1,z2)) -> SPLIT#(z0,z2) - Weak TRS: f_1(pair(z0,z1),z2,z3,z4) -> f_2(lt(z2,z3),z2,z3,z4,z0,z1) f_2(false(),z0,z1,z2,z3,z4) -> pair(add(z1,z3),z4) f_2(true(),z0,z1,z2,z3,z4) -> pair(z3,add(z1,z4)) lt(0(),s(z0)) -> true() lt(s(z0),0()) -> false() lt(s(z0),s(z1)) -> lt(z0,z1) split(z0,add(z1,z2)) -> f_1(split(z0,z2),z0,z1,z2) split(z0,nil()) -> pair(nil(),nil()) - Signature: {APPEND/2,F_1/4,F_2/6,F_3/3,LT/2,QSORT/1,SPLIT/2,append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2,APPEND#/2 ,F_1#/4,F_2#/6,F_3#/3,LT#/2,QSORT#/1,SPLIT#/2,append#/2,f_1#/4,f_2#/6,f_3#/3,lt#/2,qsort#/1,split#/2} / {0/0 ,add/2,c/0,c1/0,c10/0,c11/2,c12/2,c13/2,c2/1,c3/0,c4/1,c5/0,c6/2,c7/2,c8/0,c9/0,false/0,nil/0,pair/2,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0,c_15/1 ,c_16/0,c_17/2,c_18/0,c_19/0,c_20/3,c_21/0,c_22/0,c_23/1,c_24/2,c_25/0,c_26/2,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND#,F_1#,F_2#,F_3#,LT#,QSORT#,SPLIT#,append#,f_1# ,f_2#,f_3#,lt#,qsort#,split#} and constructors {0,add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false,nil ,pair,s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^3))