WORST_CASE(?,O(n^2)) * Step 1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #less(@x,@y) -> #cklt(#compare(@x,@y)) findMin(@l) -> findMin#1(@l) findMin#1(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) minSort(@l) -> minSort#1(findMin(@l)) minSort#1(::(@x,@xs)) -> ::(@x,minSort(@xs)) minSort#1(nil()) -> nil() - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt,#compare,#less,findMin,findMin#1,findMin#2 ,findMin#3,minSort,minSort#1} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#cklt) = {1}, uargs(::) = {2}, uargs(findMin#2) = {1}, uargs(findMin#3) = {1}, uargs(minSort#1) = {1} Following symbols are considered usable: {#cklt,#compare,#less,findMin,findMin#1,findMin#2,findMin#3,minSort,minSort#1} TcT has computed the following interpretation: p(#0) = [0] [0] p(#EQ) = [1] [4] p(#GT) = [1] [0] p(#LT) = [1] [0] p(#cklt) = [4 0] x1 + [0] [0 1] [0] p(#compare) = [0 0] x1 + [0 0] x2 + [1] [2 3] [2 0] [4] p(#false) = [4] [0] p(#less) = [0 0] x1 + [0 0] x2 + [5] [4 3] [2 0] [4] p(#neg) = [1 4] x1 + [0] [0 1] [3] p(#pos) = [1 4] x1 + [0] [0 0] [2] p(#s) = [1 4] x1 + [0] [0 0] [1] p(#true) = [4] [0] p(::) = [1 3] x2 + [1] [0 1] [3] p(findMin) = [1 2] x1 + [1] [0 1] [0] p(findMin#1) = [1 2] x1 + [0] [0 1] [0] p(findMin#2) = [1 3] x1 + [5] [0 1] [3] p(findMin#3) = [2 0] x1 + [1 6] x4 + [4] [0 0] [0 1] [6] p(minSort) = [3 7] x1 + [7] [0 1] [0] p(minSort#1) = [3 1] x1 + [3] [0 1] [0] p(nil) = [1] [3] Following rules are strictly oriented: #less(@x,@y) = [0 0] @x + [0 0] @y + [5] [4 3] [2 0] [4] > [0 0] @x + [0 0] @y + [4] [2 3] [2 0] [4] = #cklt(#compare(@x,@y)) findMin(@l) = [1 2] @l + [1] [0 1] [0] > [1 2] @l + [0] [0 1] [0] = findMin#1(@l) findMin#1(::(@x,@xs)) = [1 5] @xs + [7] [0 1] [3] > [1 5] @xs + [6] [0 1] [3] = findMin#2(findMin(@xs),@x) findMin#1(nil()) = [7] [3] > [1] [3] = nil() findMin#2(::(@y,@ys),@x) = [1 6] @ys + [15] [0 1] [6] > [1 6] @ys + [14] [0 1] [6] = findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) = [15] [6] > [11] [6] = ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) = [1 6] @ys + [12] [0 1] [6] > [1 6] @ys + [11] [0 1] [6] = ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) = [1 6] @ys + [12] [0 1] [6] > [1 6] @ys + [11] [0 1] [6] = ::(@x,::(@y,@ys)) minSort(@l) = [3 7] @l + [7] [0 1] [0] > [3 7] @l + [6] [0 1] [0] = minSort#1(findMin(@l)) minSort#1(::(@x,@xs)) = [3 10] @xs + [9] [0 1] [3] > [3 10] @xs + [8] [0 1] [3] = ::(@x,minSort(@xs)) minSort#1(nil()) = [9] [3] > [1] [3] = nil() Following rules are (at-least) weakly oriented: #cklt(#EQ()) = [4] [4] >= [4] [0] = #false() #cklt(#GT()) = [4] [0] >= [4] [0] = #false() #cklt(#LT()) = [4] [0] >= [4] [0] = #true() #compare(#0(),#0()) = [1] [4] >= [1] [4] = #EQ() #compare(#0(),#neg(@y)) = [0 0] @y + [1] [2 8] [4] >= [1] [0] = #GT() #compare(#0(),#pos(@y)) = [0 0] @y + [1] [2 8] [4] >= [1] [0] = #LT() #compare(#0(),#s(@y)) = [0 0] @y + [1] [2 8] [4] >= [1] [0] = #LT() #compare(#neg(@x),#0()) = [0 0] @x + [1] [2 11] [13] >= [1] [0] = #LT() #compare(#neg(@x),#neg(@y)) = [0 0] @x + [0 0] @y + [1] [2 11] [2 8] [13] >= [0 0] @x + [0 0] @y + [1] [2 0] [2 3] [4] = #compare(@y,@x) #compare(#neg(@x),#pos(@y)) = [0 0] @x + [0 0] @y + [1] [2 11] [2 8] [13] >= [1] [0] = #LT() #compare(#pos(@x),#0()) = [0 0] @x + [1] [2 8] [10] >= [1] [0] = #GT() #compare(#pos(@x),#neg(@y)) = [0 0] @x + [0 0] @y + [1] [2 8] [2 8] [10] >= [1] [0] = #GT() #compare(#pos(@x),#pos(@y)) = [0 0] @x + [0 0] @y + [1] [2 8] [2 8] [10] >= [0 0] @x + [0 0] @y + [1] [2 3] [2 0] [4] = #compare(@x,@y) #compare(#s(@x),#0()) = [0 0] @x + [1] [2 8] [7] >= [1] [0] = #GT() #compare(#s(@x),#s(@y)) = [0 0] @x + [0 0] @y + [1] [2 8] [2 8] [7] >= [0 0] @x + [0 0] @y + [1] [2 3] [2 0] [4] = #compare(@x,@y) WORST_CASE(?,O(n^2))