WORST_CASE(?,O(n^2)) * Step 1: WeightGap 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: 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: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [2] p(#GT) = [3] p(#LT) = [2] p(#cklt) = [1] x1 + [0] p(#compare) = [3] p(#false) = [0] p(#less) = [0] p(#neg) = [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [2] p(::) = [1] x2 + [0] p(findMin) = [0] p(findMin#1) = [0] p(findMin#2) = [1] x1 + [0] p(findMin#3) = [1] x1 + [1] x4 + [0] p(minSort) = [0] p(minSort#1) = [1] x1 + [5] p(nil) = [0] Following rules are strictly oriented: findMin#3(#true(),@x,@y,@ys) = [1] @ys + [2] > [1] @ys + [0] = ::(@x,::(@y,@ys)) minSort#1(::(@x,@xs)) = [1] @xs + [5] > [0] = ::(@x,minSort(@xs)) minSort#1(nil()) = [5] > [0] = nil() Following rules are (at-least) weakly oriented: #cklt(#EQ()) = [2] >= [0] = #false() #cklt(#GT()) = [3] >= [0] = #false() #cklt(#LT()) = [2] >= [2] = #true() #compare(#0(),#0()) = [3] >= [2] = #EQ() #compare(#0(),#neg(@y)) = [3] >= [3] = #GT() #compare(#0(),#pos(@y)) = [3] >= [2] = #LT() #compare(#0(),#s(@y)) = [3] >= [2] = #LT() #compare(#neg(@x),#0()) = [3] >= [2] = #LT() #compare(#neg(@x),#neg(@y)) = [3] >= [3] = #compare(@y,@x) #compare(#neg(@x),#pos(@y)) = [3] >= [2] = #LT() #compare(#pos(@x),#0()) = [3] >= [3] = #GT() #compare(#pos(@x),#neg(@y)) = [3] >= [3] = #GT() #compare(#pos(@x),#pos(@y)) = [3] >= [3] = #compare(@x,@y) #compare(#s(@x),#0()) = [3] >= [3] = #GT() #compare(#s(@x),#s(@y)) = [3] >= [3] = #compare(@x,@y) #less(@x,@y) = [0] >= [3] = #cklt(#compare(@x,@y)) findMin(@l) = [0] >= [0] = findMin#1(@l) findMin#1(::(@x,@xs)) = [0] >= [0] = findMin#2(findMin(@xs),@x) findMin#1(nil()) = [0] >= [0] = nil() findMin#2(::(@y,@ys),@x) = [1] @ys + [0] >= [1] @ys + [0] = findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) = [0] >= [0] = ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) = [1] @ys + [0] >= [1] @ys + [0] = ::(@y,::(@x,@ys)) minSort(@l) = [0] >= [5] = minSort#1(findMin(@l)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: WeightGap 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)) minSort(@l) -> minSort#1(findMin(@l)) - 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) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) minSort#1(::(@x,@xs)) -> ::(@x,minSort(@xs)) minSort#1(nil()) -> nil() - 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: 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: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [2] p(#GT) = [2] p(#LT) = [0] p(#cklt) = [1] x1 + [0] p(#compare) = [2] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [0] p(findMin) = [7] p(findMin#1) = [5] p(findMin#2) = [1] x1 + [0] p(findMin#3) = [1] x1 + [1] x4 + [0] p(minSort) = [2] p(minSort#1) = [1] x1 + [2] p(nil) = [2] Following rules are strictly oriented: findMin(@l) = [7] > [5] = findMin#1(@l) findMin#1(nil()) = [5] > [2] = nil() Following rules are (at-least) weakly oriented: #cklt(#EQ()) = [2] >= [0] = #false() #cklt(#GT()) = [2] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [2] >= [2] = #EQ() #compare(#0(),#neg(@y)) = [2] >= [2] = #GT() #compare(#0(),#pos(@y)) = [2] >= [0] = #LT() #compare(#0(),#s(@y)) = [2] >= [0] = #LT() #compare(#neg(@x),#0()) = [2] >= [0] = #LT() #compare(#neg(@x),#neg(@y)) = [2] >= [2] = #compare(@y,@x) #compare(#neg(@x),#pos(@y)) = [2] >= [0] = #LT() #compare(#pos(@x),#0()) = [2] >= [2] = #GT() #compare(#pos(@x),#neg(@y)) = [2] >= [2] = #GT() #compare(#pos(@x),#pos(@y)) = [2] >= [2] = #compare(@x,@y) #compare(#s(@x),#0()) = [2] >= [2] = #GT() #compare(#s(@x),#s(@y)) = [2] >= [2] = #compare(@x,@y) #less(@x,@y) = [0] >= [2] = #cklt(#compare(@x,@y)) findMin#1(::(@x,@xs)) = [5] >= [7] = findMin#2(findMin(@xs),@x) findMin#2(::(@y,@ys),@x) = [1] @ys + [0] >= [1] @ys + [0] = findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) = [2] >= [2] = ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) = [1] @ys + [0] >= [1] @ys + [0] = ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) = [1] @ys + [0] >= [1] @ys + [0] = ::(@x,::(@y,@ys)) minSort(@l) = [2] >= [9] = minSort#1(findMin(@l)) minSort#1(::(@x,@xs)) = [1] @xs + [2] >= [2] = ::(@x,minSort(@xs)) minSort#1(nil()) = [4] >= [2] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #less(@x,@y) -> #cklt(#compare(@x,@y)) findMin#1(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) 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)) minSort(@l) -> minSort#1(findMin(@l)) - 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) findMin(@l) -> findMin#1(@l) findMin#1(nil()) -> nil() findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) minSort#1(::(@x,@xs)) -> ::(@x,minSort(@xs)) minSort#1(nil()) -> nil() - 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: 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: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [1] p(#GT) = [2] p(#LT) = [1] p(#cklt) = [1] x1 + [4] p(#compare) = [3] p(#false) = [5] p(#less) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [4] p(::) = [1] x2 + [4] p(findMin) = [5] p(findMin#1) = [4] p(findMin#2) = [1] x1 + [0] p(findMin#3) = [1] x1 + [1] x4 + [4] p(minSort) = [1] x1 + [0] p(minSort#1) = [1] x1 + [0] p(nil) = [0] Following rules are strictly oriented: findMin#3(#false(),@x,@y,@ys) = [1] @ys + [9] > [1] @ys + [8] = ::(@y,::(@x,@ys)) Following rules are (at-least) weakly oriented: #cklt(#EQ()) = [5] >= [5] = #false() #cklt(#GT()) = [6] >= [5] = #false() #cklt(#LT()) = [5] >= [4] = #true() #compare(#0(),#0()) = [3] >= [1] = #EQ() #compare(#0(),#neg(@y)) = [3] >= [2] = #GT() #compare(#0(),#pos(@y)) = [3] >= [1] = #LT() #compare(#0(),#s(@y)) = [3] >= [1] = #LT() #compare(#neg(@x),#0()) = [3] >= [1] = #LT() #compare(#neg(@x),#neg(@y)) = [3] >= [3] = #compare(@y,@x) #compare(#neg(@x),#pos(@y)) = [3] >= [1] = #LT() #compare(#pos(@x),#0()) = [3] >= [2] = #GT() #compare(#pos(@x),#neg(@y)) = [3] >= [2] = #GT() #compare(#pos(@x),#pos(@y)) = [3] >= [3] = #compare(@x,@y) #compare(#s(@x),#0()) = [3] >= [2] = #GT() #compare(#s(@x),#s(@y)) = [3] >= [3] = #compare(@x,@y) #less(@x,@y) = [0] >= [7] = #cklt(#compare(@x,@y)) findMin(@l) = [5] >= [4] = findMin#1(@l) findMin#1(::(@x,@xs)) = [4] >= [5] = findMin#2(findMin(@xs),@x) findMin#1(nil()) = [4] >= [0] = nil() findMin#2(::(@y,@ys),@x) = [1] @ys + [4] >= [1] @ys + [4] = findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) = [0] >= [4] = ::(@x,nil()) findMin#3(#true(),@x,@y,@ys) = [1] @ys + [8] >= [1] @ys + [8] = ::(@x,::(@y,@ys)) minSort(@l) = [1] @l + [0] >= [5] = minSort#1(findMin(@l)) minSort#1(::(@x,@xs)) = [1] @xs + [4] >= [1] @xs + [4] = ::(@x,minSort(@xs)) minSort#1(nil()) = [0] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #less(@x,@y) -> #cklt(#compare(@x,@y)) findMin#1(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) minSort(@l) -> minSort#1(findMin(@l)) - 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) findMin(@l) -> findMin#1(@l) findMin#1(nil()) -> nil() findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) minSort#1(::(@x,@xs)) -> ::(@x,minSort(@xs)) minSort#1(nil()) -> nil() - 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: 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: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [0] p(#GT) = [1] p(#LT) = [1] p(#cklt) = [1] x1 + [0] p(#compare) = [1] p(#false) = [0] p(#less) = [0] p(#neg) = [0] p(#pos) = [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [0] p(findMin) = [7] p(findMin#1) = [4] p(findMin#2) = [1] x1 + [5] p(findMin#3) = [1] x1 + [1] x4 + [0] p(minSort) = [0] p(minSort#1) = [1] x1 + [0] p(nil) = [0] Following rules are strictly oriented: findMin#2(::(@y,@ys),@x) = [1] @ys + [5] > [1] @ys + [0] = findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) = [5] > [0] = ::(@x,nil()) Following rules are (at-least) weakly oriented: #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [1] >= [0] = #false() #cklt(#LT()) = [1] >= [0] = #true() #compare(#0(),#0()) = [1] >= [0] = #EQ() #compare(#0(),#neg(@y)) = [1] >= [1] = #GT() #compare(#0(),#pos(@y)) = [1] >= [1] = #LT() #compare(#0(),#s(@y)) = [1] >= [1] = #LT() #compare(#neg(@x),#0()) = [1] >= [1] = #LT() #compare(#neg(@x),#neg(@y)) = [1] >= [1] = #compare(@y,@x) #compare(#neg(@x),#pos(@y)) = [1] >= [1] = #LT() #compare(#pos(@x),#0()) = [1] >= [1] = #GT() #compare(#pos(@x),#neg(@y)) = [1] >= [1] = #GT() #compare(#pos(@x),#pos(@y)) = [1] >= [1] = #compare(@x,@y) #compare(#s(@x),#0()) = [1] >= [1] = #GT() #compare(#s(@x),#s(@y)) = [1] >= [1] = #compare(@x,@y) #less(@x,@y) = [0] >= [1] = #cklt(#compare(@x,@y)) findMin(@l) = [7] >= [4] = findMin#1(@l) findMin#1(::(@x,@xs)) = [4] >= [12] = findMin#2(findMin(@xs),@x) findMin#1(nil()) = [4] >= [0] = nil() findMin#3(#false(),@x,@y,@ys) = [1] @ys + [0] >= [1] @ys + [0] = ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) = [1] @ys + [0] >= [1] @ys + [0] = ::(@x,::(@y,@ys)) minSort(@l) = [0] >= [7] = minSort#1(findMin(@l)) minSort#1(::(@x,@xs)) = [1] @xs + [0] >= [0] = ::(@x,minSort(@xs)) minSort#1(nil()) = [0] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 5: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #less(@x,@y) -> #cklt(#compare(@x,@y)) findMin#1(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) minSort(@l) -> minSort#1(findMin(@l)) - 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) findMin(@l) -> findMin#1(@l) 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#1(::(@x,@xs)) -> ::(@x,minSort(@xs)) minSort#1(nil()) -> nil() - 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: 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: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [2] p(#GT) = [0] p(#LT) = [1] p(#cklt) = [1] x1 + [1] p(#compare) = [2] p(#false) = [0] p(#less) = [4] p(#neg) = [1] x1 + [0] p(#pos) = [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [0] p(findMin) = [6] p(findMin#1) = [2] p(findMin#2) = [1] x1 + [4] p(findMin#3) = [1] x1 + [1] x4 + [0] p(minSort) = [1] x1 + [0] p(minSort#1) = [1] x1 + [1] p(nil) = [1] Following rules are strictly oriented: #less(@x,@y) = [4] > [3] = #cklt(#compare(@x,@y)) Following rules are (at-least) weakly oriented: #cklt(#EQ()) = [3] >= [0] = #false() #cklt(#GT()) = [1] >= [0] = #false() #cklt(#LT()) = [2] >= [0] = #true() #compare(#0(),#0()) = [2] >= [2] = #EQ() #compare(#0(),#neg(@y)) = [2] >= [0] = #GT() #compare(#0(),#pos(@y)) = [2] >= [1] = #LT() #compare(#0(),#s(@y)) = [2] >= [1] = #LT() #compare(#neg(@x),#0()) = [2] >= [1] = #LT() #compare(#neg(@x),#neg(@y)) = [2] >= [2] = #compare(@y,@x) #compare(#neg(@x),#pos(@y)) = [2] >= [1] = #LT() #compare(#pos(@x),#0()) = [2] >= [0] = #GT() #compare(#pos(@x),#neg(@y)) = [2] >= [0] = #GT() #compare(#pos(@x),#pos(@y)) = [2] >= [2] = #compare(@x,@y) #compare(#s(@x),#0()) = [2] >= [0] = #GT() #compare(#s(@x),#s(@y)) = [2] >= [2] = #compare(@x,@y) findMin(@l) = [6] >= [2] = findMin#1(@l) findMin#1(::(@x,@xs)) = [2] >= [10] = findMin#2(findMin(@xs),@x) findMin#1(nil()) = [2] >= [1] = nil() findMin#2(::(@y,@ys),@x) = [1] @ys + [4] >= [1] @ys + [4] = findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) = [5] >= [1] = ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) = [1] @ys + [0] >= [1] @ys + [0] = ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) = [1] @ys + [0] >= [1] @ys + [0] = ::(@x,::(@y,@ys)) minSort(@l) = [1] @l + [0] >= [7] = minSort#1(findMin(@l)) minSort#1(::(@x,@xs)) = [1] @xs + [1] >= [1] @xs + [0] = ::(@x,minSort(@xs)) minSort#1(nil()) = [2] >= [1] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 6: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: findMin#1(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) minSort(@l) -> minSort#1(findMin(@l)) - 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) #less(@x,@y) -> #cklt(#compare(@x,@y)) findMin(@l) -> findMin#1(@l) 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#1(::(@x,@xs)) -> ::(@x,minSort(@xs)) minSort#1(nil()) -> nil() - 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 = 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(#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] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#cklt) = [8] x1 + [0] p(#compare) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [2] p(#pos) = [1] p(#s) = [1] p(#true) = [0] p(::) = [1] x2 + [1] p(findMin) = [1] x1 + [0] p(findMin#1) = [1] x1 + [0] p(findMin#2) = [1] x1 + [1] p(findMin#3) = [4] x1 + [1] x4 + [2] p(minSort) = [8] x1 + [8] p(minSort#1) = [8] x1 + [1] p(nil) = [0] Following rules are strictly oriented: minSort(@l) = [8] @l + [8] > [8] @l + [1] = minSort#1(findMin(@l)) Following rules are (at-least) weakly oriented: #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [0] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(@y)) = [0] >= [0] = #GT() #compare(#0(),#pos(@y)) = [0] >= [0] = #LT() #compare(#0(),#s(@y)) = [0] >= [0] = #LT() #compare(#neg(@x),#0()) = [0] >= [0] = #LT() #compare(#neg(@x),#neg(@y)) = [0] >= [0] = #compare(@y,@x) #compare(#neg(@x),#pos(@y)) = [0] >= [0] = #LT() #compare(#pos(@x),#0()) = [0] >= [0] = #GT() #compare(#pos(@x),#neg(@y)) = [0] >= [0] = #GT() #compare(#pos(@x),#pos(@y)) = [0] >= [0] = #compare(@x,@y) #compare(#s(@x),#0()) = [0] >= [0] = #GT() #compare(#s(@x),#s(@y)) = [0] >= [0] = #compare(@x,@y) #less(@x,@y) = [0] >= [0] = #cklt(#compare(@x,@y)) findMin(@l) = [1] @l + [0] >= [1] @l + [0] = findMin#1(@l) findMin#1(::(@x,@xs)) = [1] @xs + [1] >= [1] @xs + [1] = findMin#2(findMin(@xs),@x) findMin#1(nil()) = [0] >= [0] = nil() findMin#2(::(@y,@ys),@x) = [1] @ys + [2] >= [1] @ys + [2] = findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) = [1] >= [1] = ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) = [1] @ys + [2] >= [1] @ys + [2] = ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) = [1] @ys + [2] >= [1] @ys + [2] = ::(@x,::(@y,@ys)) minSort#1(::(@x,@xs)) = [8] @xs + [9] >= [8] @xs + [9] = ::(@x,minSort(@xs)) minSort#1(nil()) = [1] >= [0] = nil() * Step 7: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: findMin#1(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) - 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) #less(@x,@y) -> #cklt(#compare(@x,@y)) findMin(@l) -> findMin#1(@l) 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() - 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 = Just any strict-rules} + 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] [1] p(#EQ) = [6] [0] p(#GT) = [6] [0] p(#LT) = [6] [6] p(#cklt) = [1 0] x1 + [0] [0 1] [1] p(#compare) = [0 0] x1 + [0 0] x2 + [6] [4 4] [4 4] [1] p(#false) = [6] [1] p(#less) = [0 0] x1 + [0 0] x2 + [6] [4 4] [4 4] [2] p(#neg) = [1 0] x1 + [0] [0 1] [1] p(#pos) = [1 1] x1 + [0] [0 1] [1] p(#s) = [1 1] x1 + [0] [0 1] [1] p(#true) = [6] [0] p(::) = [1 3] x2 + [0] [0 1] [2] p(findMin) = [1 1] x1 + [1] [0 1] [0] p(findMin#1) = [1 1] x1 + [0] [0 1] [0] p(findMin#2) = [1 3] x1 + [0] [0 1] [2] p(findMin#3) = [1 0] x1 + [1 6] x4 + [0] [0 0] [0 1] [4] p(minSort) = [2 6] x1 + [6] [0 1] [1] p(minSort#1) = [2 4] x1 + [1] [0 1] [1] p(nil) = [0] [2] Following rules are strictly oriented: findMin#1(::(@x,@xs)) = [1 4] @xs + [2] [0 1] [2] > [1 4] @xs + [1] [0 1] [2] = findMin#2(findMin(@xs),@x) Following rules are (at-least) weakly oriented: #cklt(#EQ()) = [6] [1] >= [6] [1] = #false() #cklt(#GT()) = [6] [1] >= [6] [1] = #false() #cklt(#LT()) = [6] [7] >= [6] [0] = #true() #compare(#0(),#0()) = [6] [9] >= [6] [0] = #EQ() #compare(#0(),#neg(@y)) = [0 0] @y + [6] [4 4] [9] >= [6] [0] = #GT() #compare(#0(),#pos(@y)) = [0 0] @y + [6] [4 8] [9] >= [6] [6] = #LT() #compare(#0(),#s(@y)) = [0 0] @y + [6] [4 8] [9] >= [6] [6] = #LT() #compare(#neg(@x),#0()) = [0 0] @x + [6] [4 4] [9] >= [6] [6] = #LT() #compare(#neg(@x),#neg(@y)) = [0 0] @x + [0 0] @y + [6] [4 4] [4 4] [9] >= [0 0] @x + [0 0] @y + [6] [4 4] [4 4] [1] = #compare(@y,@x) #compare(#neg(@x),#pos(@y)) = [0 0] @x + [0 0] @y + [6] [4 4] [4 8] [9] >= [6] [6] = #LT() #compare(#pos(@x),#0()) = [0 0] @x + [6] [4 8] [9] >= [6] [0] = #GT() #compare(#pos(@x),#neg(@y)) = [0 0] @x + [0 0] @y + [6] [4 8] [4 4] [9] >= [6] [0] = #GT() #compare(#pos(@x),#pos(@y)) = [0 0] @x + [0 0] @y + [6] [4 8] [4 8] [9] >= [0 0] @x + [0 0] @y + [6] [4 4] [4 4] [1] = #compare(@x,@y) #compare(#s(@x),#0()) = [0 0] @x + [6] [4 8] [9] >= [6] [0] = #GT() #compare(#s(@x),#s(@y)) = [0 0] @x + [0 0] @y + [6] [4 8] [4 8] [9] >= [0 0] @x + [0 0] @y + [6] [4 4] [4 4] [1] = #compare(@x,@y) #less(@x,@y) = [0 0] @x + [0 0] @y + [6] [4 4] [4 4] [2] >= [0 0] @x + [0 0] @y + [6] [4 4] [4 4] [2] = #cklt(#compare(@x,@y)) findMin(@l) = [1 1] @l + [1] [0 1] [0] >= [1 1] @l + [0] [0 1] [0] = findMin#1(@l) findMin#1(nil()) = [2] [2] >= [0] [2] = nil() findMin#2(::(@y,@ys),@x) = [1 6] @ys + [6] [0 1] [4] >= [1 6] @ys + [6] [0 1] [4] = findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) = [6] [4] >= [6] [4] = ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) = [1 6] @ys + [6] [0 1] [4] >= [1 6] @ys + [6] [0 1] [4] = ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) = [1 6] @ys + [6] [0 1] [4] >= [1 6] @ys + [6] [0 1] [4] = ::(@x,::(@y,@ys)) minSort(@l) = [2 6] @l + [6] [0 1] [1] >= [2 6] @l + [3] [0 1] [1] = minSort#1(findMin(@l)) minSort#1(::(@x,@xs)) = [2 10] @xs + [9] [0 1] [3] >= [2 9] @xs + [9] [0 1] [3] = ::(@x,minSort(@xs)) minSort#1(nil()) = [9] [3] >= [0] [2] = nil() * Step 8: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - 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) #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() - 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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))