WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: cond_partition_pivot_heap_1(False(),x3,E(),x2,x1) -> Pair(E(),T(E(),x2,x1)) cond_partition_pivot_heap_1(False(),x6,T(x5,x4,x3),x2,x1) -> cond_partition_pivot_heap_7(leqElem#2(x4,x6) ,x6 ,x2 ,x1 ,x5 ,x4 ,x3) cond_partition_pivot_heap_1(True(),x3,x2,x1,E()) -> Pair(T(x2,x1,E()),E()) cond_partition_pivot_heap_1(True(),x6,x5,x4,T(x3,x2,x1)) -> cond_partition_pivot_heap_3(leqElem#2(x2,x6) ,x6 ,x5 ,x4 ,x3 ,x2 ,x1) cond_partition_pivot_heap_3(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_5(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_3(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_4(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) cond_partition_pivot_heap_4(Pair(x12,x13),x6,x7,x9,x10) -> Pair(T(T(x6,x7,x9),x10,x12),x13) cond_partition_pivot_heap_5(Pair(x12,x13),x6,x7,x10,x11) -> Pair(T(x6,x7,x12),T(x13,x10,x11)) cond_partition_pivot_heap_7(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_9(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_7(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_8(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) cond_partition_pivot_heap_8(Pair(x12,x13),x7,x8,x9,x10) -> Pair(T(x9,x10,x12),T(x13,x7,x8)) cond_partition_pivot_heap_9(Pair(x12,x13),x7,x8,x10,x11) -> Pair(x12,T(x13,x10,T(x11,x7,x8))) leq#2(0(),x12) -> True() leq#2(S(x16),0()) -> False() leq#2(S(x4),S(x2)) -> leq#2(x4,x2) leqElem#2(Elem(x4),Elem(x2)) -> leq#2(x4,x2) main(x2,x1) -> partition#2(x1,x2) partition#2(x2,E()) -> Pair(E(),E()) partition#2(x8,T(x6,x4,x2)) -> cond_partition_pivot_heap_1(leqElem#2(x4,x8),x8,x6,x4,x2) - Signature: {cond_partition_pivot_heap_1/5,cond_partition_pivot_heap_3/7,cond_partition_pivot_heap_4/5 ,cond_partition_pivot_heap_5/5,cond_partition_pivot_heap_7/7,cond_partition_pivot_heap_8/5 ,cond_partition_pivot_heap_9/5,leq#2/2,leqElem#2/2,main/2,partition#2/2} / {0/0,E/0,Elem/1,False/0,Pair/2 ,S/1,T/3,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_partition_pivot_heap_1,cond_partition_pivot_heap_3 ,cond_partition_pivot_heap_4,cond_partition_pivot_heap_5,cond_partition_pivot_heap_7 ,cond_partition_pivot_heap_8,cond_partition_pivot_heap_9,leq#2,leqElem#2,main ,partition#2} and constructors {0,E,Elem,False,Pair,S,T,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(cond_partition_pivot_heap_1) = {1}, uargs(cond_partition_pivot_heap_3) = {1}, uargs(cond_partition_pivot_heap_4) = {1}, uargs(cond_partition_pivot_heap_5) = {1}, uargs(cond_partition_pivot_heap_7) = {1}, uargs(cond_partition_pivot_heap_8) = {1}, uargs(cond_partition_pivot_heap_9) = {1} Following symbols are considered usable: {cond_partition_pivot_heap_1,cond_partition_pivot_heap_3,cond_partition_pivot_heap_4 ,cond_partition_pivot_heap_5,cond_partition_pivot_heap_7,cond_partition_pivot_heap_8 ,cond_partition_pivot_heap_9,leq#2,leqElem#2,main,partition#2} TcT has computed the following interpretation: p(0) = [0] p(E) = [0] p(Elem) = [2] p(False) = [0] p(Pair) = [0] p(S) = [1] p(T) = [1] x1 + [1] x3 + [2] p(True) = [0] p(cond_partition_pivot_heap_1) = [4] x1 + [4] x3 + [4] x5 + [0] p(cond_partition_pivot_heap_3) = [2] x1 + [2] x3 + [4] x5 + [4] x7 + [0] p(cond_partition_pivot_heap_4) = [1] x1 + [2] x2 + [0] p(cond_partition_pivot_heap_5) = [1] x1 + [2] x2 + [4] x5 + [0] p(cond_partition_pivot_heap_7) = [1] x1 + [4] x4 + [4] x5 + [4] x7 + [4] p(cond_partition_pivot_heap_8) = [1] x1 + [4] x3 + [4] x4 + [4] p(cond_partition_pivot_heap_9) = [1] x1 + [4] x3 + [1] p(leq#2) = [0] p(leqElem#2) = [0] p(main) = [4] x1 + [2] x2 + [0] p(partition#2) = [4] x2 + [0] Following rules are strictly oriented: cond_partition_pivot_heap_1(False(),x6,T(x5,x4,x3),x2,x1) = [4] x1 + [4] x3 + [4] x5 + [8] > [4] x1 + [4] x3 + [4] x5 + [4] = cond_partition_pivot_heap_7(leqElem#2(x4,x6),x6,x2,x1,x5,x4,x3) cond_partition_pivot_heap_1(True(),x6,x5,x4,T(x3,x2,x1)) = [4] x1 + [4] x3 + [4] x5 + [8] > [4] x1 + [4] x3 + [2] x5 + [0] = cond_partition_pivot_heap_3(leqElem#2(x2,x6),x6,x5,x4,x3,x2,x1) cond_partition_pivot_heap_7(False(),x6,x5,x4,x3,x2,x1) = [4] x1 + [4] x3 + [4] x4 + [4] > [4] x3 + [4] x4 + [1] = cond_partition_pivot_heap_9(partition#2(x6,x3),x5,x4,x2,x1) cond_partition_pivot_heap_8(Pair(x12,x13),x7,x8,x9,x10) = [4] x8 + [4] x9 + [4] > [0] = Pair(T(x9,x10,x12),T(x13,x7,x8)) cond_partition_pivot_heap_9(Pair(x12,x13),x7,x8,x10,x11) = [4] x8 + [1] > [0] = Pair(x12,T(x13,x10,T(x11,x7,x8))) partition#2(x8,T(x6,x4,x2)) = [4] x2 + [4] x6 + [8] > [4] x2 + [4] x6 + [0] = cond_partition_pivot_heap_1(leqElem#2(x4,x8),x8,x6,x4,x2) Following rules are (at-least) weakly oriented: cond_partition_pivot_heap_1(False(),x3,E(),x2,x1) = [4] x1 + [0] >= [0] = Pair(E(),T(E(),x2,x1)) cond_partition_pivot_heap_1(True(),x3,x2,x1,E()) = [4] x2 + [0] >= [0] = Pair(T(x2,x1,E()),E()) cond_partition_pivot_heap_3(False(),x6,x5,x4,x3,x2,x1) = [4] x1 + [4] x3 + [2] x5 + [0] >= [4] x1 + [4] x3 + [2] x5 + [0] = cond_partition_pivot_heap_5(partition#2(x6,x3),x5,x4,x2,x1) cond_partition_pivot_heap_3(True(),x6,x5,x4,x3,x2,x1) = [4] x1 + [4] x3 + [2] x5 + [0] >= [4] x1 + [2] x5 + [0] = cond_partition_pivot_heap_4(partition#2(x6,x1),x5,x4,x3,x2) cond_partition_pivot_heap_4(Pair(x12,x13),x6,x7,x9,x10) = [2] x6 + [0] >= [0] = Pair(T(T(x6,x7,x9),x10,x12),x13) cond_partition_pivot_heap_5(Pair(x12,x13),x6,x7,x10,x11) = [4] x11 + [2] x6 + [0] >= [0] = Pair(T(x6,x7,x12),T(x13,x10,x11)) cond_partition_pivot_heap_7(True(),x6,x5,x4,x3,x2,x1) = [4] x1 + [4] x3 + [4] x4 + [4] >= [4] x1 + [4] x3 + [4] x4 + [4] = cond_partition_pivot_heap_8(partition#2(x6,x1),x5,x4,x3,x2) leq#2(0(),x12) = [0] >= [0] = True() leq#2(S(x16),0()) = [0] >= [0] = False() leq#2(S(x4),S(x2)) = [0] >= [0] = leq#2(x4,x2) leqElem#2(Elem(x4),Elem(x2)) = [0] >= [0] = leq#2(x4,x2) main(x2,x1) = [2] x1 + [4] x2 + [0] >= [4] x2 + [0] = partition#2(x1,x2) partition#2(x2,E()) = [0] >= [0] = Pair(E(),E()) * Step 2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: cond_partition_pivot_heap_1(False(),x3,E(),x2,x1) -> Pair(E(),T(E(),x2,x1)) cond_partition_pivot_heap_1(True(),x3,x2,x1,E()) -> Pair(T(x2,x1,E()),E()) cond_partition_pivot_heap_3(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_5(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_3(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_4(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) cond_partition_pivot_heap_4(Pair(x12,x13),x6,x7,x9,x10) -> Pair(T(T(x6,x7,x9),x10,x12),x13) cond_partition_pivot_heap_5(Pair(x12,x13),x6,x7,x10,x11) -> Pair(T(x6,x7,x12),T(x13,x10,x11)) cond_partition_pivot_heap_7(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_8(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) leq#2(0(),x12) -> True() leq#2(S(x16),0()) -> False() leq#2(S(x4),S(x2)) -> leq#2(x4,x2) leqElem#2(Elem(x4),Elem(x2)) -> leq#2(x4,x2) main(x2,x1) -> partition#2(x1,x2) partition#2(x2,E()) -> Pair(E(),E()) - Weak TRS: cond_partition_pivot_heap_1(False(),x6,T(x5,x4,x3),x2,x1) -> cond_partition_pivot_heap_7(leqElem#2(x4,x6) ,x6 ,x2 ,x1 ,x5 ,x4 ,x3) cond_partition_pivot_heap_1(True(),x6,x5,x4,T(x3,x2,x1)) -> cond_partition_pivot_heap_3(leqElem#2(x2,x6) ,x6 ,x5 ,x4 ,x3 ,x2 ,x1) cond_partition_pivot_heap_7(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_9(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_8(Pair(x12,x13),x7,x8,x9,x10) -> Pair(T(x9,x10,x12),T(x13,x7,x8)) cond_partition_pivot_heap_9(Pair(x12,x13),x7,x8,x10,x11) -> Pair(x12,T(x13,x10,T(x11,x7,x8))) partition#2(x8,T(x6,x4,x2)) -> cond_partition_pivot_heap_1(leqElem#2(x4,x8),x8,x6,x4,x2) - Signature: {cond_partition_pivot_heap_1/5,cond_partition_pivot_heap_3/7,cond_partition_pivot_heap_4/5 ,cond_partition_pivot_heap_5/5,cond_partition_pivot_heap_7/7,cond_partition_pivot_heap_8/5 ,cond_partition_pivot_heap_9/5,leq#2/2,leqElem#2/2,main/2,partition#2/2} / {0/0,E/0,Elem/1,False/0,Pair/2 ,S/1,T/3,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_partition_pivot_heap_1,cond_partition_pivot_heap_3 ,cond_partition_pivot_heap_4,cond_partition_pivot_heap_5,cond_partition_pivot_heap_7 ,cond_partition_pivot_heap_8,cond_partition_pivot_heap_9,leq#2,leqElem#2,main ,partition#2} and constructors {0,E,Elem,False,Pair,S,T,True} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(cond_partition_pivot_heap_1) = {1}, uargs(cond_partition_pivot_heap_3) = {1}, uargs(cond_partition_pivot_heap_4) = {1}, uargs(cond_partition_pivot_heap_5) = {1}, uargs(cond_partition_pivot_heap_7) = {1}, uargs(cond_partition_pivot_heap_8) = {1}, uargs(cond_partition_pivot_heap_9) = {1} Following symbols are considered usable: {cond_partition_pivot_heap_1,cond_partition_pivot_heap_3,cond_partition_pivot_heap_4 ,cond_partition_pivot_heap_5,cond_partition_pivot_heap_7,cond_partition_pivot_heap_8 ,cond_partition_pivot_heap_9,leq#2,leqElem#2,main,partition#2} TcT has computed the following interpretation: p(0) = 0 p(E) = 0 p(Elem) = x1 p(False) = 0 p(Pair) = 0 p(S) = 0 p(T) = 2 + x2 p(True) = 0 p(cond_partition_pivot_heap_1) = 2*x1 p(cond_partition_pivot_heap_3) = x1 p(cond_partition_pivot_heap_4) = 4*x1 p(cond_partition_pivot_heap_5) = x1 p(cond_partition_pivot_heap_7) = x1 p(cond_partition_pivot_heap_8) = 4*x1 p(cond_partition_pivot_heap_9) = 2*x1 p(leq#2) = 0 p(leqElem#2) = 0 p(main) = 1 + 2*x1 p(partition#2) = 0 Following rules are strictly oriented: main(x2,x1) = 1 + 2*x2 > 0 = partition#2(x1,x2) Following rules are (at-least) weakly oriented: cond_partition_pivot_heap_1(False(),x3,E(),x2,x1) = 0 >= 0 = Pair(E(),T(E(),x2,x1)) cond_partition_pivot_heap_1(False(),x6,T(x5,x4,x3),x2,x1) = 0 >= 0 = cond_partition_pivot_heap_7(leqElem#2(x4,x6),x6,x2,x1,x5,x4,x3) cond_partition_pivot_heap_1(True(),x3,x2,x1,E()) = 0 >= 0 = Pair(T(x2,x1,E()),E()) cond_partition_pivot_heap_1(True(),x6,x5,x4,T(x3,x2,x1)) = 0 >= 0 = cond_partition_pivot_heap_3(leqElem#2(x2,x6),x6,x5,x4,x3,x2,x1) cond_partition_pivot_heap_3(False(),x6,x5,x4,x3,x2,x1) = 0 >= 0 = cond_partition_pivot_heap_5(partition#2(x6,x3),x5,x4,x2,x1) cond_partition_pivot_heap_3(True(),x6,x5,x4,x3,x2,x1) = 0 >= 0 = cond_partition_pivot_heap_4(partition#2(x6,x1),x5,x4,x3,x2) cond_partition_pivot_heap_4(Pair(x12,x13),x6,x7,x9,x10) = 0 >= 0 = Pair(T(T(x6,x7,x9),x10,x12),x13) cond_partition_pivot_heap_5(Pair(x12,x13),x6,x7,x10,x11) = 0 >= 0 = Pair(T(x6,x7,x12),T(x13,x10,x11)) cond_partition_pivot_heap_7(False(),x6,x5,x4,x3,x2,x1) = 0 >= 0 = cond_partition_pivot_heap_9(partition#2(x6,x3),x5,x4,x2,x1) cond_partition_pivot_heap_7(True(),x6,x5,x4,x3,x2,x1) = 0 >= 0 = cond_partition_pivot_heap_8(partition#2(x6,x1),x5,x4,x3,x2) cond_partition_pivot_heap_8(Pair(x12,x13),x7,x8,x9,x10) = 0 >= 0 = Pair(T(x9,x10,x12),T(x13,x7,x8)) cond_partition_pivot_heap_9(Pair(x12,x13),x7,x8,x10,x11) = 0 >= 0 = Pair(x12,T(x13,x10,T(x11,x7,x8))) leq#2(0(),x12) = 0 >= 0 = True() leq#2(S(x16),0()) = 0 >= 0 = False() leq#2(S(x4),S(x2)) = 0 >= 0 = leq#2(x4,x2) leqElem#2(Elem(x4),Elem(x2)) = 0 >= 0 = leq#2(x4,x2) partition#2(x2,E()) = 0 >= 0 = Pair(E(),E()) partition#2(x8,T(x6,x4,x2)) = 0 >= 0 = cond_partition_pivot_heap_1(leqElem#2(x4,x8),x8,x6,x4,x2) * Step 3: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: cond_partition_pivot_heap_1(False(),x3,E(),x2,x1) -> Pair(E(),T(E(),x2,x1)) cond_partition_pivot_heap_1(True(),x3,x2,x1,E()) -> Pair(T(x2,x1,E()),E()) cond_partition_pivot_heap_3(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_5(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_3(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_4(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) cond_partition_pivot_heap_4(Pair(x12,x13),x6,x7,x9,x10) -> Pair(T(T(x6,x7,x9),x10,x12),x13) cond_partition_pivot_heap_5(Pair(x12,x13),x6,x7,x10,x11) -> Pair(T(x6,x7,x12),T(x13,x10,x11)) cond_partition_pivot_heap_7(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_8(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) leq#2(0(),x12) -> True() leq#2(S(x16),0()) -> False() leq#2(S(x4),S(x2)) -> leq#2(x4,x2) leqElem#2(Elem(x4),Elem(x2)) -> leq#2(x4,x2) partition#2(x2,E()) -> Pair(E(),E()) - Weak TRS: cond_partition_pivot_heap_1(False(),x6,T(x5,x4,x3),x2,x1) -> cond_partition_pivot_heap_7(leqElem#2(x4,x6) ,x6 ,x2 ,x1 ,x5 ,x4 ,x3) cond_partition_pivot_heap_1(True(),x6,x5,x4,T(x3,x2,x1)) -> cond_partition_pivot_heap_3(leqElem#2(x2,x6) ,x6 ,x5 ,x4 ,x3 ,x2 ,x1) cond_partition_pivot_heap_7(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_9(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_8(Pair(x12,x13),x7,x8,x9,x10) -> Pair(T(x9,x10,x12),T(x13,x7,x8)) cond_partition_pivot_heap_9(Pair(x12,x13),x7,x8,x10,x11) -> Pair(x12,T(x13,x10,T(x11,x7,x8))) main(x2,x1) -> partition#2(x1,x2) partition#2(x8,T(x6,x4,x2)) -> cond_partition_pivot_heap_1(leqElem#2(x4,x8),x8,x6,x4,x2) - Signature: {cond_partition_pivot_heap_1/5,cond_partition_pivot_heap_3/7,cond_partition_pivot_heap_4/5 ,cond_partition_pivot_heap_5/5,cond_partition_pivot_heap_7/7,cond_partition_pivot_heap_8/5 ,cond_partition_pivot_heap_9/5,leq#2/2,leqElem#2/2,main/2,partition#2/2} / {0/0,E/0,Elem/1,False/0,Pair/2 ,S/1,T/3,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_partition_pivot_heap_1,cond_partition_pivot_heap_3 ,cond_partition_pivot_heap_4,cond_partition_pivot_heap_5,cond_partition_pivot_heap_7 ,cond_partition_pivot_heap_8,cond_partition_pivot_heap_9,leq#2,leqElem#2,main ,partition#2} and constructors {0,E,Elem,False,Pair,S,T,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(cond_partition_pivot_heap_1) = {1}, uargs(cond_partition_pivot_heap_3) = {1}, uargs(cond_partition_pivot_heap_4) = {1}, uargs(cond_partition_pivot_heap_5) = {1}, uargs(cond_partition_pivot_heap_7) = {1}, uargs(cond_partition_pivot_heap_8) = {1}, uargs(cond_partition_pivot_heap_9) = {1} Following symbols are considered usable: {cond_partition_pivot_heap_1,cond_partition_pivot_heap_3,cond_partition_pivot_heap_4 ,cond_partition_pivot_heap_5,cond_partition_pivot_heap_7,cond_partition_pivot_heap_8 ,cond_partition_pivot_heap_9,leq#2,leqElem#2,main,partition#2} TcT has computed the following interpretation: p(0) = [2] p(E) = [4] p(Elem) = [0] p(False) = [0] p(Pair) = [0] p(S) = [4] p(T) = [1] x1 + [1] x3 + [3] p(True) = [0] p(cond_partition_pivot_heap_1) = [2] x1 + [1] x3 + [1] x5 + [1] p(cond_partition_pivot_heap_3) = [2] x1 + [1] x3 + [1] x5 + [1] x7 + [2] p(cond_partition_pivot_heap_4) = [1] x1 + [1] x2 + [0] p(cond_partition_pivot_heap_5) = [1] x1 + [1] x5 + [0] p(cond_partition_pivot_heap_7) = [1] x1 + [1] x4 + [1] x5 + [1] x7 + [1] p(cond_partition_pivot_heap_8) = [1] x1 + [1] p(cond_partition_pivot_heap_9) = [1] x1 + [1] x5 + [0] p(leq#2) = [0] p(leqElem#2) = [1] p(main) = [4] x1 + [4] x2 + [1] p(partition#2) = [1] x2 + [0] Following rules are strictly oriented: cond_partition_pivot_heap_1(False(),x3,E(),x2,x1) = [1] x1 + [5] > [0] = Pair(E(),T(E(),x2,x1)) cond_partition_pivot_heap_1(True(),x3,x2,x1,E()) = [1] x2 + [5] > [0] = Pair(T(x2,x1,E()),E()) cond_partition_pivot_heap_3(False(),x6,x5,x4,x3,x2,x1) = [1] x1 + [1] x3 + [1] x5 + [2] > [1] x1 + [1] x3 + [0] = cond_partition_pivot_heap_5(partition#2(x6,x3),x5,x4,x2,x1) cond_partition_pivot_heap_3(True(),x6,x5,x4,x3,x2,x1) = [1] x1 + [1] x3 + [1] x5 + [2] > [1] x1 + [1] x5 + [0] = cond_partition_pivot_heap_4(partition#2(x6,x1),x5,x4,x3,x2) leqElem#2(Elem(x4),Elem(x2)) = [1] > [0] = leq#2(x4,x2) partition#2(x2,E()) = [4] > [0] = Pair(E(),E()) Following rules are (at-least) weakly oriented: cond_partition_pivot_heap_1(False(),x6,T(x5,x4,x3),x2,x1) = [1] x1 + [1] x3 + [1] x5 + [4] >= [1] x1 + [1] x3 + [1] x5 + [2] = cond_partition_pivot_heap_7(leqElem#2(x4,x6),x6,x2,x1,x5,x4,x3) cond_partition_pivot_heap_1(True(),x6,x5,x4,T(x3,x2,x1)) = [1] x1 + [1] x3 + [1] x5 + [4] >= [1] x1 + [1] x3 + [1] x5 + [4] = cond_partition_pivot_heap_3(leqElem#2(x2,x6),x6,x5,x4,x3,x2,x1) cond_partition_pivot_heap_4(Pair(x12,x13),x6,x7,x9,x10) = [1] x6 + [0] >= [0] = Pair(T(T(x6,x7,x9),x10,x12),x13) cond_partition_pivot_heap_5(Pair(x12,x13),x6,x7,x10,x11) = [1] x11 + [0] >= [0] = Pair(T(x6,x7,x12),T(x13,x10,x11)) cond_partition_pivot_heap_7(False(),x6,x5,x4,x3,x2,x1) = [1] x1 + [1] x3 + [1] x4 + [1] >= [1] x1 + [1] x3 + [0] = cond_partition_pivot_heap_9(partition#2(x6,x3),x5,x4,x2,x1) cond_partition_pivot_heap_7(True(),x6,x5,x4,x3,x2,x1) = [1] x1 + [1] x3 + [1] x4 + [1] >= [1] x1 + [1] = cond_partition_pivot_heap_8(partition#2(x6,x1),x5,x4,x3,x2) cond_partition_pivot_heap_8(Pair(x12,x13),x7,x8,x9,x10) = [1] >= [0] = Pair(T(x9,x10,x12),T(x13,x7,x8)) cond_partition_pivot_heap_9(Pair(x12,x13),x7,x8,x10,x11) = [1] x11 + [0] >= [0] = Pair(x12,T(x13,x10,T(x11,x7,x8))) leq#2(0(),x12) = [0] >= [0] = True() leq#2(S(x16),0()) = [0] >= [0] = False() leq#2(S(x4),S(x2)) = [0] >= [0] = leq#2(x4,x2) main(x2,x1) = [4] x1 + [4] x2 + [1] >= [1] x2 + [0] = partition#2(x1,x2) partition#2(x8,T(x6,x4,x2)) = [1] x2 + [1] x6 + [3] >= [1] x2 + [1] x6 + [3] = cond_partition_pivot_heap_1(leqElem#2(x4,x8),x8,x6,x4,x2) * Step 4: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: cond_partition_pivot_heap_4(Pair(x12,x13),x6,x7,x9,x10) -> Pair(T(T(x6,x7,x9),x10,x12),x13) cond_partition_pivot_heap_5(Pair(x12,x13),x6,x7,x10,x11) -> Pair(T(x6,x7,x12),T(x13,x10,x11)) cond_partition_pivot_heap_7(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_8(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) leq#2(0(),x12) -> True() leq#2(S(x16),0()) -> False() leq#2(S(x4),S(x2)) -> leq#2(x4,x2) - Weak TRS: cond_partition_pivot_heap_1(False(),x3,E(),x2,x1) -> Pair(E(),T(E(),x2,x1)) cond_partition_pivot_heap_1(False(),x6,T(x5,x4,x3),x2,x1) -> cond_partition_pivot_heap_7(leqElem#2(x4,x6) ,x6 ,x2 ,x1 ,x5 ,x4 ,x3) cond_partition_pivot_heap_1(True(),x3,x2,x1,E()) -> Pair(T(x2,x1,E()),E()) cond_partition_pivot_heap_1(True(),x6,x5,x4,T(x3,x2,x1)) -> cond_partition_pivot_heap_3(leqElem#2(x2,x6) ,x6 ,x5 ,x4 ,x3 ,x2 ,x1) cond_partition_pivot_heap_3(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_5(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_3(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_4(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) cond_partition_pivot_heap_7(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_9(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_8(Pair(x12,x13),x7,x8,x9,x10) -> Pair(T(x9,x10,x12),T(x13,x7,x8)) cond_partition_pivot_heap_9(Pair(x12,x13),x7,x8,x10,x11) -> Pair(x12,T(x13,x10,T(x11,x7,x8))) leqElem#2(Elem(x4),Elem(x2)) -> leq#2(x4,x2) main(x2,x1) -> partition#2(x1,x2) partition#2(x2,E()) -> Pair(E(),E()) partition#2(x8,T(x6,x4,x2)) -> cond_partition_pivot_heap_1(leqElem#2(x4,x8),x8,x6,x4,x2) - Signature: {cond_partition_pivot_heap_1/5,cond_partition_pivot_heap_3/7,cond_partition_pivot_heap_4/5 ,cond_partition_pivot_heap_5/5,cond_partition_pivot_heap_7/7,cond_partition_pivot_heap_8/5 ,cond_partition_pivot_heap_9/5,leq#2/2,leqElem#2/2,main/2,partition#2/2} / {0/0,E/0,Elem/1,False/0,Pair/2 ,S/1,T/3,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_partition_pivot_heap_1,cond_partition_pivot_heap_3 ,cond_partition_pivot_heap_4,cond_partition_pivot_heap_5,cond_partition_pivot_heap_7 ,cond_partition_pivot_heap_8,cond_partition_pivot_heap_9,leq#2,leqElem#2,main ,partition#2} and constructors {0,E,Elem,False,Pair,S,T,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(cond_partition_pivot_heap_1) = {1}, uargs(cond_partition_pivot_heap_3) = {1}, uargs(cond_partition_pivot_heap_4) = {1}, uargs(cond_partition_pivot_heap_5) = {1}, uargs(cond_partition_pivot_heap_7) = {1}, uargs(cond_partition_pivot_heap_8) = {1}, uargs(cond_partition_pivot_heap_9) = {1} Following symbols are considered usable: {cond_partition_pivot_heap_1,cond_partition_pivot_heap_3,cond_partition_pivot_heap_4 ,cond_partition_pivot_heap_5,cond_partition_pivot_heap_7,cond_partition_pivot_heap_8 ,cond_partition_pivot_heap_9,leq#2,leqElem#2,main,partition#2} TcT has computed the following interpretation: p(0) = [1] p(E) = [6] p(Elem) = [0] p(False) = [0] p(Pair) = [0] p(S) = [0] p(T) = [1] x1 + [1] x2 + [1] x3 + [5] p(True) = [0] p(cond_partition_pivot_heap_1) = [1] x1 + [1] x3 + [1] x4 + [1] x5 + [3] p(cond_partition_pivot_heap_3) = [4] x1 + [1] x4 + [1] x5 + [1] x6 + [1] x7 + [0] p(cond_partition_pivot_heap_4) = [1] x1 + [1] x3 + [1] x5 + [0] p(cond_partition_pivot_heap_5) = [1] x1 + [1] x4 + [0] p(cond_partition_pivot_heap_7) = [2] x1 + [1] x4 + [1] x5 + [1] x7 + [3] p(cond_partition_pivot_heap_8) = [1] x1 + [0] p(cond_partition_pivot_heap_9) = [1] x1 + [1] x3 + [1] x5 + [3] p(leq#2) = [0] p(leqElem#2) = [2] p(main) = [4] x1 + [0] p(partition#2) = [1] x2 + [0] Following rules are strictly oriented: cond_partition_pivot_heap_7(True(),x6,x5,x4,x3,x2,x1) = [1] x1 + [1] x3 + [1] x4 + [3] > [1] x1 + [0] = cond_partition_pivot_heap_8(partition#2(x6,x1),x5,x4,x3,x2) Following rules are (at-least) weakly oriented: cond_partition_pivot_heap_1(False(),x3,E(),x2,x1) = [1] x1 + [1] x2 + [9] >= [0] = Pair(E(),T(E(),x2,x1)) cond_partition_pivot_heap_1(False(),x6,T(x5,x4,x3),x2,x1) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [1] x5 + [8] >= [1] x1 + [1] x3 + [1] x5 + [7] = cond_partition_pivot_heap_7(leqElem#2(x4,x6),x6,x2,x1,x5,x4,x3) cond_partition_pivot_heap_1(True(),x3,x2,x1,E()) = [1] x1 + [1] x2 + [9] >= [0] = Pair(T(x2,x1,E()),E()) cond_partition_pivot_heap_1(True(),x6,x5,x4,T(x3,x2,x1)) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [1] x5 + [8] >= [1] x1 + [1] x2 + [1] x3 + [1] x4 + [8] = cond_partition_pivot_heap_3(leqElem#2(x2,x6),x6,x5,x4,x3,x2,x1) cond_partition_pivot_heap_3(False(),x6,x5,x4,x3,x2,x1) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] >= [1] x2 + [1] x3 + [0] = cond_partition_pivot_heap_5(partition#2(x6,x3),x5,x4,x2,x1) cond_partition_pivot_heap_3(True(),x6,x5,x4,x3,x2,x1) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] >= [1] x1 + [1] x2 + [1] x4 + [0] = cond_partition_pivot_heap_4(partition#2(x6,x1),x5,x4,x3,x2) cond_partition_pivot_heap_4(Pair(x12,x13),x6,x7,x9,x10) = [1] x10 + [1] x7 + [0] >= [0] = Pair(T(T(x6,x7,x9),x10,x12),x13) cond_partition_pivot_heap_5(Pair(x12,x13),x6,x7,x10,x11) = [1] x10 + [0] >= [0] = Pair(T(x6,x7,x12),T(x13,x10,x11)) cond_partition_pivot_heap_7(False(),x6,x5,x4,x3,x2,x1) = [1] x1 + [1] x3 + [1] x4 + [3] >= [1] x1 + [1] x3 + [1] x4 + [3] = cond_partition_pivot_heap_9(partition#2(x6,x3),x5,x4,x2,x1) cond_partition_pivot_heap_8(Pair(x12,x13),x7,x8,x9,x10) = [0] >= [0] = Pair(T(x9,x10,x12),T(x13,x7,x8)) cond_partition_pivot_heap_9(Pair(x12,x13),x7,x8,x10,x11) = [1] x11 + [1] x8 + [3] >= [0] = Pair(x12,T(x13,x10,T(x11,x7,x8))) leq#2(0(),x12) = [0] >= [0] = True() leq#2(S(x16),0()) = [0] >= [0] = False() leq#2(S(x4),S(x2)) = [0] >= [0] = leq#2(x4,x2) leqElem#2(Elem(x4),Elem(x2)) = [2] >= [0] = leq#2(x4,x2) main(x2,x1) = [4] x2 + [0] >= [1] x2 + [0] = partition#2(x1,x2) partition#2(x2,E()) = [6] >= [0] = Pair(E(),E()) partition#2(x8,T(x6,x4,x2)) = [1] x2 + [1] x4 + [1] x6 + [5] >= [1] x2 + [1] x4 + [1] x6 + [5] = cond_partition_pivot_heap_1(leqElem#2(x4,x8),x8,x6,x4,x2) * Step 5: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: cond_partition_pivot_heap_4(Pair(x12,x13),x6,x7,x9,x10) -> Pair(T(T(x6,x7,x9),x10,x12),x13) cond_partition_pivot_heap_5(Pair(x12,x13),x6,x7,x10,x11) -> Pair(T(x6,x7,x12),T(x13,x10,x11)) leq#2(0(),x12) -> True() leq#2(S(x16),0()) -> False() leq#2(S(x4),S(x2)) -> leq#2(x4,x2) - Weak TRS: cond_partition_pivot_heap_1(False(),x3,E(),x2,x1) -> Pair(E(),T(E(),x2,x1)) cond_partition_pivot_heap_1(False(),x6,T(x5,x4,x3),x2,x1) -> cond_partition_pivot_heap_7(leqElem#2(x4,x6) ,x6 ,x2 ,x1 ,x5 ,x4 ,x3) cond_partition_pivot_heap_1(True(),x3,x2,x1,E()) -> Pair(T(x2,x1,E()),E()) cond_partition_pivot_heap_1(True(),x6,x5,x4,T(x3,x2,x1)) -> cond_partition_pivot_heap_3(leqElem#2(x2,x6) ,x6 ,x5 ,x4 ,x3 ,x2 ,x1) cond_partition_pivot_heap_3(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_5(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_3(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_4(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) cond_partition_pivot_heap_7(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_9(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_7(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_8(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) cond_partition_pivot_heap_8(Pair(x12,x13),x7,x8,x9,x10) -> Pair(T(x9,x10,x12),T(x13,x7,x8)) cond_partition_pivot_heap_9(Pair(x12,x13),x7,x8,x10,x11) -> Pair(x12,T(x13,x10,T(x11,x7,x8))) leqElem#2(Elem(x4),Elem(x2)) -> leq#2(x4,x2) main(x2,x1) -> partition#2(x1,x2) partition#2(x2,E()) -> Pair(E(),E()) partition#2(x8,T(x6,x4,x2)) -> cond_partition_pivot_heap_1(leqElem#2(x4,x8),x8,x6,x4,x2) - Signature: {cond_partition_pivot_heap_1/5,cond_partition_pivot_heap_3/7,cond_partition_pivot_heap_4/5 ,cond_partition_pivot_heap_5/5,cond_partition_pivot_heap_7/7,cond_partition_pivot_heap_8/5 ,cond_partition_pivot_heap_9/5,leq#2/2,leqElem#2/2,main/2,partition#2/2} / {0/0,E/0,Elem/1,False/0,Pair/2 ,S/1,T/3,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_partition_pivot_heap_1,cond_partition_pivot_heap_3 ,cond_partition_pivot_heap_4,cond_partition_pivot_heap_5,cond_partition_pivot_heap_7 ,cond_partition_pivot_heap_8,cond_partition_pivot_heap_9,leq#2,leqElem#2,main ,partition#2} and constructors {0,E,Elem,False,Pair,S,T,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(cond_partition_pivot_heap_1) = {1}, uargs(cond_partition_pivot_heap_3) = {1}, uargs(cond_partition_pivot_heap_4) = {1}, uargs(cond_partition_pivot_heap_5) = {1}, uargs(cond_partition_pivot_heap_7) = {1}, uargs(cond_partition_pivot_heap_8) = {1}, uargs(cond_partition_pivot_heap_9) = {1} Following symbols are considered usable: {cond_partition_pivot_heap_1,cond_partition_pivot_heap_3,cond_partition_pivot_heap_4 ,cond_partition_pivot_heap_5,cond_partition_pivot_heap_7,cond_partition_pivot_heap_8 ,cond_partition_pivot_heap_9,leq#2,leqElem#2,main,partition#2} TcT has computed the following interpretation: p(0) = [0] p(E) = [4] p(Elem) = [1] x1 + [0] p(False) = [0] p(Pair) = [0] p(S) = [1] x1 + [0] p(T) = [1] x1 + [1] x3 + [4] p(True) = [0] p(cond_partition_pivot_heap_1) = [4] x1 + [2] x3 + [2] x5 + [4] p(cond_partition_pivot_heap_3) = [5] x1 + [2] x3 + [2] x5 + [2] x7 + [7] p(cond_partition_pivot_heap_4) = [1] x1 + [4] p(cond_partition_pivot_heap_5) = [1] x1 + [2] x2 + [0] p(cond_partition_pivot_heap_7) = [1] x1 + [2] x4 + [2] x5 + [2] x7 + [0] p(cond_partition_pivot_heap_8) = [1] x1 + [1] x4 + [0] p(cond_partition_pivot_heap_9) = [1] x1 + [1] x3 + [0] p(leq#2) = [1] p(leqElem#2) = [1] p(main) = [2] x1 + [4] p(partition#2) = [2] x2 + [0] Following rules are strictly oriented: cond_partition_pivot_heap_4(Pair(x12,x13),x6,x7,x9,x10) = [4] > [0] = Pair(T(T(x6,x7,x9),x10,x12),x13) leq#2(0(),x12) = [1] > [0] = True() leq#2(S(x16),0()) = [1] > [0] = False() Following rules are (at-least) weakly oriented: cond_partition_pivot_heap_1(False(),x3,E(),x2,x1) = [2] x1 + [12] >= [0] = Pair(E(),T(E(),x2,x1)) cond_partition_pivot_heap_1(False(),x6,T(x5,x4,x3),x2,x1) = [2] x1 + [2] x3 + [2] x5 + [12] >= [2] x1 + [2] x3 + [2] x5 + [1] = cond_partition_pivot_heap_7(leqElem#2(x4,x6),x6,x2,x1,x5,x4,x3) cond_partition_pivot_heap_1(True(),x3,x2,x1,E()) = [2] x2 + [12] >= [0] = Pair(T(x2,x1,E()),E()) cond_partition_pivot_heap_1(True(),x6,x5,x4,T(x3,x2,x1)) = [2] x1 + [2] x3 + [2] x5 + [12] >= [2] x1 + [2] x3 + [2] x5 + [12] = cond_partition_pivot_heap_3(leqElem#2(x2,x6),x6,x5,x4,x3,x2,x1) cond_partition_pivot_heap_3(False(),x6,x5,x4,x3,x2,x1) = [2] x1 + [2] x3 + [2] x5 + [7] >= [2] x3 + [2] x5 + [0] = cond_partition_pivot_heap_5(partition#2(x6,x3),x5,x4,x2,x1) cond_partition_pivot_heap_3(True(),x6,x5,x4,x3,x2,x1) = [2] x1 + [2] x3 + [2] x5 + [7] >= [2] x1 + [4] = cond_partition_pivot_heap_4(partition#2(x6,x1),x5,x4,x3,x2) cond_partition_pivot_heap_5(Pair(x12,x13),x6,x7,x10,x11) = [2] x6 + [0] >= [0] = Pair(T(x6,x7,x12),T(x13,x10,x11)) cond_partition_pivot_heap_7(False(),x6,x5,x4,x3,x2,x1) = [2] x1 + [2] x3 + [2] x4 + [0] >= [2] x3 + [1] x4 + [0] = cond_partition_pivot_heap_9(partition#2(x6,x3),x5,x4,x2,x1) cond_partition_pivot_heap_7(True(),x6,x5,x4,x3,x2,x1) = [2] x1 + [2] x3 + [2] x4 + [0] >= [2] x1 + [1] x3 + [0] = cond_partition_pivot_heap_8(partition#2(x6,x1),x5,x4,x3,x2) cond_partition_pivot_heap_8(Pair(x12,x13),x7,x8,x9,x10) = [1] x9 + [0] >= [0] = Pair(T(x9,x10,x12),T(x13,x7,x8)) cond_partition_pivot_heap_9(Pair(x12,x13),x7,x8,x10,x11) = [1] x8 + [0] >= [0] = Pair(x12,T(x13,x10,T(x11,x7,x8))) leq#2(S(x4),S(x2)) = [1] >= [1] = leq#2(x4,x2) leqElem#2(Elem(x4),Elem(x2)) = [1] >= [1] = leq#2(x4,x2) main(x2,x1) = [2] x2 + [4] >= [2] x2 + [0] = partition#2(x1,x2) partition#2(x2,E()) = [8] >= [0] = Pair(E(),E()) partition#2(x8,T(x6,x4,x2)) = [2] x2 + [2] x6 + [8] >= [2] x2 + [2] x6 + [8] = cond_partition_pivot_heap_1(leqElem#2(x4,x8),x8,x6,x4,x2) * Step 6: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: cond_partition_pivot_heap_5(Pair(x12,x13),x6,x7,x10,x11) -> Pair(T(x6,x7,x12),T(x13,x10,x11)) leq#2(S(x4),S(x2)) -> leq#2(x4,x2) - Weak TRS: cond_partition_pivot_heap_1(False(),x3,E(),x2,x1) -> Pair(E(),T(E(),x2,x1)) cond_partition_pivot_heap_1(False(),x6,T(x5,x4,x3),x2,x1) -> cond_partition_pivot_heap_7(leqElem#2(x4,x6) ,x6 ,x2 ,x1 ,x5 ,x4 ,x3) cond_partition_pivot_heap_1(True(),x3,x2,x1,E()) -> Pair(T(x2,x1,E()),E()) cond_partition_pivot_heap_1(True(),x6,x5,x4,T(x3,x2,x1)) -> cond_partition_pivot_heap_3(leqElem#2(x2,x6) ,x6 ,x5 ,x4 ,x3 ,x2 ,x1) cond_partition_pivot_heap_3(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_5(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_3(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_4(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) cond_partition_pivot_heap_4(Pair(x12,x13),x6,x7,x9,x10) -> Pair(T(T(x6,x7,x9),x10,x12),x13) cond_partition_pivot_heap_7(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_9(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_7(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_8(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) cond_partition_pivot_heap_8(Pair(x12,x13),x7,x8,x9,x10) -> Pair(T(x9,x10,x12),T(x13,x7,x8)) cond_partition_pivot_heap_9(Pair(x12,x13),x7,x8,x10,x11) -> Pair(x12,T(x13,x10,T(x11,x7,x8))) leq#2(0(),x12) -> True() leq#2(S(x16),0()) -> False() leqElem#2(Elem(x4),Elem(x2)) -> leq#2(x4,x2) main(x2,x1) -> partition#2(x1,x2) partition#2(x2,E()) -> Pair(E(),E()) partition#2(x8,T(x6,x4,x2)) -> cond_partition_pivot_heap_1(leqElem#2(x4,x8),x8,x6,x4,x2) - Signature: {cond_partition_pivot_heap_1/5,cond_partition_pivot_heap_3/7,cond_partition_pivot_heap_4/5 ,cond_partition_pivot_heap_5/5,cond_partition_pivot_heap_7/7,cond_partition_pivot_heap_8/5 ,cond_partition_pivot_heap_9/5,leq#2/2,leqElem#2/2,main/2,partition#2/2} / {0/0,E/0,Elem/1,False/0,Pair/2 ,S/1,T/3,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_partition_pivot_heap_1,cond_partition_pivot_heap_3 ,cond_partition_pivot_heap_4,cond_partition_pivot_heap_5,cond_partition_pivot_heap_7 ,cond_partition_pivot_heap_8,cond_partition_pivot_heap_9,leq#2,leqElem#2,main ,partition#2} and constructors {0,E,Elem,False,Pair,S,T,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(cond_partition_pivot_heap_1) = {1}, uargs(cond_partition_pivot_heap_3) = {1}, uargs(cond_partition_pivot_heap_4) = {1}, uargs(cond_partition_pivot_heap_5) = {1}, uargs(cond_partition_pivot_heap_7) = {1}, uargs(cond_partition_pivot_heap_8) = {1}, uargs(cond_partition_pivot_heap_9) = {1} Following symbols are considered usable: {cond_partition_pivot_heap_1,cond_partition_pivot_heap_3,cond_partition_pivot_heap_4 ,cond_partition_pivot_heap_5,cond_partition_pivot_heap_7,cond_partition_pivot_heap_8 ,cond_partition_pivot_heap_9,leq#2,leqElem#2,main,partition#2} TcT has computed the following interpretation: p(0) = [1] p(E) = [2] p(Elem) = [2] p(False) = [1] p(Pair) = [4] p(S) = [1] p(T) = [1] x1 + [1] x2 + [1] x3 + [2] p(True) = [1] p(cond_partition_pivot_heap_1) = [2] x1 + [1] x2 + [4] x3 + [4] x5 + [4] p(cond_partition_pivot_heap_3) = [1] x1 + [1] x2 + [1] x3 + [4] x5 + [2] x6 + [4] x7 + [3] p(cond_partition_pivot_heap_4) = [1] x1 + [2] x5 + [1] p(cond_partition_pivot_heap_5) = [1] x1 + [2] x4 + [1] x5 + [4] p(cond_partition_pivot_heap_7) = [1] x1 + [1] x2 + [4] x4 + [4] x5 + [1] x6 + [4] x7 + [3] p(cond_partition_pivot_heap_8) = [1] x1 + [4] p(cond_partition_pivot_heap_9) = [1] x1 + [4] x3 + [1] x5 + [2] p(leq#2) = [4] p(leqElem#2) = [2] x1 + [0] p(main) = [4] x1 + [4] x2 + [0] p(partition#2) = [1] x1 + [4] x2 + [0] Following rules are strictly oriented: cond_partition_pivot_heap_5(Pair(x12,x13),x6,x7,x10,x11) = [2] x10 + [1] x11 + [8] > [4] = Pair(T(x6,x7,x12),T(x13,x10,x11)) Following rules are (at-least) weakly oriented: cond_partition_pivot_heap_1(False(),x3,E(),x2,x1) = [4] x1 + [1] x3 + [14] >= [4] = Pair(E(),T(E(),x2,x1)) cond_partition_pivot_heap_1(False(),x6,T(x5,x4,x3),x2,x1) = [4] x1 + [4] x3 + [4] x4 + [4] x5 + [1] x6 + [14] >= [4] x1 + [4] x3 + [3] x4 + [4] x5 + [1] x6 + [3] = cond_partition_pivot_heap_7(leqElem#2(x4,x6),x6,x2,x1,x5,x4,x3) cond_partition_pivot_heap_1(True(),x3,x2,x1,E()) = [4] x2 + [1] x3 + [14] >= [4] = Pair(T(x2,x1,E()),E()) cond_partition_pivot_heap_1(True(),x6,x5,x4,T(x3,x2,x1)) = [4] x1 + [4] x2 + [4] x3 + [4] x5 + [1] x6 + [14] >= [4] x1 + [4] x2 + [4] x3 + [1] x5 + [1] x6 + [3] = cond_partition_pivot_heap_3(leqElem#2(x2,x6),x6,x5,x4,x3,x2,x1) cond_partition_pivot_heap_3(False(),x6,x5,x4,x3,x2,x1) = [4] x1 + [2] x2 + [4] x3 + [1] x5 + [1] x6 + [4] >= [1] x1 + [2] x2 + [4] x3 + [1] x6 + [4] = cond_partition_pivot_heap_5(partition#2(x6,x3),x5,x4,x2,x1) cond_partition_pivot_heap_3(True(),x6,x5,x4,x3,x2,x1) = [4] x1 + [2] x2 + [4] x3 + [1] x5 + [1] x6 + [4] >= [4] x1 + [2] x2 + [1] x6 + [1] = cond_partition_pivot_heap_4(partition#2(x6,x1),x5,x4,x3,x2) cond_partition_pivot_heap_4(Pair(x12,x13),x6,x7,x9,x10) = [2] x10 + [5] >= [4] = Pair(T(T(x6,x7,x9),x10,x12),x13) cond_partition_pivot_heap_7(False(),x6,x5,x4,x3,x2,x1) = [4] x1 + [1] x2 + [4] x3 + [4] x4 + [1] x6 + [4] >= [1] x1 + [4] x3 + [4] x4 + [1] x6 + [2] = cond_partition_pivot_heap_9(partition#2(x6,x3),x5,x4,x2,x1) cond_partition_pivot_heap_7(True(),x6,x5,x4,x3,x2,x1) = [4] x1 + [1] x2 + [4] x3 + [4] x4 + [1] x6 + [4] >= [4] x1 + [1] x6 + [4] = cond_partition_pivot_heap_8(partition#2(x6,x1),x5,x4,x3,x2) cond_partition_pivot_heap_8(Pair(x12,x13),x7,x8,x9,x10) = [8] >= [4] = Pair(T(x9,x10,x12),T(x13,x7,x8)) cond_partition_pivot_heap_9(Pair(x12,x13),x7,x8,x10,x11) = [1] x11 + [4] x8 + [6] >= [4] = Pair(x12,T(x13,x10,T(x11,x7,x8))) leq#2(0(),x12) = [4] >= [1] = True() leq#2(S(x16),0()) = [4] >= [1] = False() leq#2(S(x4),S(x2)) = [4] >= [4] = leq#2(x4,x2) leqElem#2(Elem(x4),Elem(x2)) = [4] >= [4] = leq#2(x4,x2) main(x2,x1) = [4] x1 + [4] x2 + [0] >= [1] x1 + [4] x2 + [0] = partition#2(x1,x2) partition#2(x2,E()) = [1] x2 + [8] >= [4] = Pair(E(),E()) partition#2(x8,T(x6,x4,x2)) = [4] x2 + [4] x4 + [4] x6 + [1] x8 + [8] >= [4] x2 + [4] x4 + [4] x6 + [1] x8 + [4] = cond_partition_pivot_heap_1(leqElem#2(x4,x8),x8,x6,x4,x2) * Step 7: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: leq#2(S(x4),S(x2)) -> leq#2(x4,x2) - Weak TRS: cond_partition_pivot_heap_1(False(),x3,E(),x2,x1) -> Pair(E(),T(E(),x2,x1)) cond_partition_pivot_heap_1(False(),x6,T(x5,x4,x3),x2,x1) -> cond_partition_pivot_heap_7(leqElem#2(x4,x6) ,x6 ,x2 ,x1 ,x5 ,x4 ,x3) cond_partition_pivot_heap_1(True(),x3,x2,x1,E()) -> Pair(T(x2,x1,E()),E()) cond_partition_pivot_heap_1(True(),x6,x5,x4,T(x3,x2,x1)) -> cond_partition_pivot_heap_3(leqElem#2(x2,x6) ,x6 ,x5 ,x4 ,x3 ,x2 ,x1) cond_partition_pivot_heap_3(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_5(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_3(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_4(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) cond_partition_pivot_heap_4(Pair(x12,x13),x6,x7,x9,x10) -> Pair(T(T(x6,x7,x9),x10,x12),x13) cond_partition_pivot_heap_5(Pair(x12,x13),x6,x7,x10,x11) -> Pair(T(x6,x7,x12),T(x13,x10,x11)) cond_partition_pivot_heap_7(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_9(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_7(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_8(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) cond_partition_pivot_heap_8(Pair(x12,x13),x7,x8,x9,x10) -> Pair(T(x9,x10,x12),T(x13,x7,x8)) cond_partition_pivot_heap_9(Pair(x12,x13),x7,x8,x10,x11) -> Pair(x12,T(x13,x10,T(x11,x7,x8))) leq#2(0(),x12) -> True() leq#2(S(x16),0()) -> False() leqElem#2(Elem(x4),Elem(x2)) -> leq#2(x4,x2) main(x2,x1) -> partition#2(x1,x2) partition#2(x2,E()) -> Pair(E(),E()) partition#2(x8,T(x6,x4,x2)) -> cond_partition_pivot_heap_1(leqElem#2(x4,x8),x8,x6,x4,x2) - Signature: {cond_partition_pivot_heap_1/5,cond_partition_pivot_heap_3/7,cond_partition_pivot_heap_4/5 ,cond_partition_pivot_heap_5/5,cond_partition_pivot_heap_7/7,cond_partition_pivot_heap_8/5 ,cond_partition_pivot_heap_9/5,leq#2/2,leqElem#2/2,main/2,partition#2/2} / {0/0,E/0,Elem/1,False/0,Pair/2 ,S/1,T/3,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_partition_pivot_heap_1,cond_partition_pivot_heap_3 ,cond_partition_pivot_heap_4,cond_partition_pivot_heap_5,cond_partition_pivot_heap_7 ,cond_partition_pivot_heap_8,cond_partition_pivot_heap_9,leq#2,leqElem#2,main ,partition#2} and constructors {0,E,Elem,False,Pair,S,T,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(cond_partition_pivot_heap_1) = {1}, uargs(cond_partition_pivot_heap_3) = {1}, uargs(cond_partition_pivot_heap_4) = {1}, uargs(cond_partition_pivot_heap_5) = {1}, uargs(cond_partition_pivot_heap_7) = {1}, uargs(cond_partition_pivot_heap_8) = {1}, uargs(cond_partition_pivot_heap_9) = {1} Following symbols are considered usable: {cond_partition_pivot_heap_1,cond_partition_pivot_heap_3,cond_partition_pivot_heap_4 ,cond_partition_pivot_heap_5,cond_partition_pivot_heap_7,cond_partition_pivot_heap_8 ,cond_partition_pivot_heap_9,leq#2,leqElem#2,main,partition#2} TcT has computed the following interpretation: p(0) = [0] p(E) = [1] p(Elem) = [1] x1 + [2] p(False) = [0] p(Pair) = [0] p(S) = [1] x1 + [2] p(T) = [1] x1 + [1] x2 + [1] x3 + [2] p(True) = [0] p(cond_partition_pivot_heap_1) = [1] x1 + [4] x3 + [4] x5 + [2] p(cond_partition_pivot_heap_3) = [1] x1 + [4] x5 + [4] x7 + [6] p(cond_partition_pivot_heap_4) = [1] x1 + [0] p(cond_partition_pivot_heap_5) = [1] x1 + [4] x5 + [0] p(cond_partition_pivot_heap_7) = [1] x1 + [4] x4 + [4] x5 + [4] x7 + [4] p(cond_partition_pivot_heap_8) = [1] x1 + [2] p(cond_partition_pivot_heap_9) = [1] x1 + [1] x3 + [4] x5 + [3] p(leq#2) = [4] x1 + [1] p(leqElem#2) = [4] x1 + [4] p(main) = [5] x1 + [2] x2 + [1] p(partition#2) = [4] x2 + [1] Following rules are strictly oriented: leq#2(S(x4),S(x2)) = [4] x4 + [9] > [4] x4 + [1] = leq#2(x4,x2) Following rules are (at-least) weakly oriented: cond_partition_pivot_heap_1(False(),x3,E(),x2,x1) = [4] x1 + [6] >= [0] = Pair(E(),T(E(),x2,x1)) cond_partition_pivot_heap_1(False(),x6,T(x5,x4,x3),x2,x1) = [4] x1 + [4] x3 + [4] x4 + [4] x5 + [10] >= [4] x1 + [4] x3 + [4] x4 + [4] x5 + [8] = cond_partition_pivot_heap_7(leqElem#2(x4,x6),x6,x2,x1,x5,x4,x3) cond_partition_pivot_heap_1(True(),x3,x2,x1,E()) = [4] x2 + [6] >= [0] = Pair(T(x2,x1,E()),E()) cond_partition_pivot_heap_1(True(),x6,x5,x4,T(x3,x2,x1)) = [4] x1 + [4] x2 + [4] x3 + [4] x5 + [10] >= [4] x1 + [4] x2 + [4] x3 + [10] = cond_partition_pivot_heap_3(leqElem#2(x2,x6),x6,x5,x4,x3,x2,x1) cond_partition_pivot_heap_3(False(),x6,x5,x4,x3,x2,x1) = [4] x1 + [4] x3 + [6] >= [4] x1 + [4] x3 + [1] = cond_partition_pivot_heap_5(partition#2(x6,x3),x5,x4,x2,x1) cond_partition_pivot_heap_3(True(),x6,x5,x4,x3,x2,x1) = [4] x1 + [4] x3 + [6] >= [4] x1 + [1] = cond_partition_pivot_heap_4(partition#2(x6,x1),x5,x4,x3,x2) cond_partition_pivot_heap_4(Pair(x12,x13),x6,x7,x9,x10) = [0] >= [0] = Pair(T(T(x6,x7,x9),x10,x12),x13) cond_partition_pivot_heap_5(Pair(x12,x13),x6,x7,x10,x11) = [4] x11 + [0] >= [0] = Pair(T(x6,x7,x12),T(x13,x10,x11)) cond_partition_pivot_heap_7(False(),x6,x5,x4,x3,x2,x1) = [4] x1 + [4] x3 + [4] x4 + [4] >= [4] x1 + [4] x3 + [1] x4 + [4] = cond_partition_pivot_heap_9(partition#2(x6,x3),x5,x4,x2,x1) cond_partition_pivot_heap_7(True(),x6,x5,x4,x3,x2,x1) = [4] x1 + [4] x3 + [4] x4 + [4] >= [4] x1 + [3] = cond_partition_pivot_heap_8(partition#2(x6,x1),x5,x4,x3,x2) cond_partition_pivot_heap_8(Pair(x12,x13),x7,x8,x9,x10) = [2] >= [0] = Pair(T(x9,x10,x12),T(x13,x7,x8)) cond_partition_pivot_heap_9(Pair(x12,x13),x7,x8,x10,x11) = [4] x11 + [1] x8 + [3] >= [0] = Pair(x12,T(x13,x10,T(x11,x7,x8))) leq#2(0(),x12) = [1] >= [0] = True() leq#2(S(x16),0()) = [4] x16 + [9] >= [0] = False() leqElem#2(Elem(x4),Elem(x2)) = [4] x4 + [12] >= [4] x4 + [1] = leq#2(x4,x2) main(x2,x1) = [2] x1 + [5] x2 + [1] >= [4] x2 + [1] = partition#2(x1,x2) partition#2(x2,E()) = [5] >= [0] = Pair(E(),E()) partition#2(x8,T(x6,x4,x2)) = [4] x2 + [4] x4 + [4] x6 + [9] >= [4] x2 + [4] x4 + [4] x6 + [6] = cond_partition_pivot_heap_1(leqElem#2(x4,x8),x8,x6,x4,x2) * Step 8: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: cond_partition_pivot_heap_1(False(),x3,E(),x2,x1) -> Pair(E(),T(E(),x2,x1)) cond_partition_pivot_heap_1(False(),x6,T(x5,x4,x3),x2,x1) -> cond_partition_pivot_heap_7(leqElem#2(x4,x6) ,x6 ,x2 ,x1 ,x5 ,x4 ,x3) cond_partition_pivot_heap_1(True(),x3,x2,x1,E()) -> Pair(T(x2,x1,E()),E()) cond_partition_pivot_heap_1(True(),x6,x5,x4,T(x3,x2,x1)) -> cond_partition_pivot_heap_3(leqElem#2(x2,x6) ,x6 ,x5 ,x4 ,x3 ,x2 ,x1) cond_partition_pivot_heap_3(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_5(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_3(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_4(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) cond_partition_pivot_heap_4(Pair(x12,x13),x6,x7,x9,x10) -> Pair(T(T(x6,x7,x9),x10,x12),x13) cond_partition_pivot_heap_5(Pair(x12,x13),x6,x7,x10,x11) -> Pair(T(x6,x7,x12),T(x13,x10,x11)) cond_partition_pivot_heap_7(False(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_9(partition#2(x6,x3) ,x5 ,x4 ,x2 ,x1) cond_partition_pivot_heap_7(True(),x6,x5,x4,x3,x2,x1) -> cond_partition_pivot_heap_8(partition#2(x6,x1) ,x5 ,x4 ,x3 ,x2) cond_partition_pivot_heap_8(Pair(x12,x13),x7,x8,x9,x10) -> Pair(T(x9,x10,x12),T(x13,x7,x8)) cond_partition_pivot_heap_9(Pair(x12,x13),x7,x8,x10,x11) -> Pair(x12,T(x13,x10,T(x11,x7,x8))) leq#2(0(),x12) -> True() leq#2(S(x16),0()) -> False() leq#2(S(x4),S(x2)) -> leq#2(x4,x2) leqElem#2(Elem(x4),Elem(x2)) -> leq#2(x4,x2) main(x2,x1) -> partition#2(x1,x2) partition#2(x2,E()) -> Pair(E(),E()) partition#2(x8,T(x6,x4,x2)) -> cond_partition_pivot_heap_1(leqElem#2(x4,x8),x8,x6,x4,x2) - Signature: {cond_partition_pivot_heap_1/5,cond_partition_pivot_heap_3/7,cond_partition_pivot_heap_4/5 ,cond_partition_pivot_heap_5/5,cond_partition_pivot_heap_7/7,cond_partition_pivot_heap_8/5 ,cond_partition_pivot_heap_9/5,leq#2/2,leqElem#2/2,main/2,partition#2/2} / {0/0,E/0,Elem/1,False/0,Pair/2 ,S/1,T/3,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond_partition_pivot_heap_1,cond_partition_pivot_heap_3 ,cond_partition_pivot_heap_4,cond_partition_pivot_heap_5,cond_partition_pivot_heap_7 ,cond_partition_pivot_heap_8,cond_partition_pivot_heap_9,leq#2,leqElem#2,main ,partition#2} and constructors {0,E,Elem,False,Pair,S,T,True} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))