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: Ara 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: Ara {heuristics_ = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> A(0, 0) #EQ :: [] -(0)-> A(0, 0) #EQ :: [] -(0)-> A(14, 14) #GT :: [] -(0)-> A(0, 0) #GT :: [] -(0)-> A(14, 14) #LT :: [] -(0)-> A(0, 0) #LT :: [] -(0)-> A(14, 14) #cklt :: [A(0, 0)] -(0)-> A(7, 7) #compare :: [A(0, 0) x A(0, 0)] -(0)-> A(14, 14) #false :: [] -(0)-> A(0, 0) #false :: [] -(0)-> A(13, 13) #less :: [A(0, 0) x A(0, 0)] -(0)-> A(1, 1) #neg :: [A(0, 0)] -(0)-> A(0, 0) #pos :: [A(0, 0)] -(0)-> A(0, 0) #s :: [A(0, 0)] -(0)-> A(0, 0) #true :: [] -(0)-> A(0, 0) #true :: [] -(0)-> A(13, 13) :: :: [A(0, 0) x A(15, 6)] -(9)-> A(9, 6) :: :: [A(0, 0) x A(14, 6)] -(8)-> A(8, 6) :: :: [A(0, 0) x A(13, 10)] -(3)-> A(3, 10) :: :: [A(0, 0) x A(9, 6)] -(3)-> A(3, 6) :: :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) findMin :: [A(14, 6)] -(8)-> A(8, 6) findMin#1 :: [A(9, 6)] -(6)-> A(3, 6) findMin#2 :: [A(9, 6) x A(0, 0)] -(3)-> A(3, 6) findMin#3 :: [A(0, 0) x A(0, 0) x A(0, 0) x A(15, 6)] -(12)-> A(3, 6) minSort :: [A(14, 6)] -(8)-> A(0, 0) minSort#1 :: [A(8, 6)] -(0)-> A(0, 0) nil :: [] -(0)-> A(9, 6) nil :: [] -(0)-> A(8, 6) nil :: [] -(0)-> A(5, 13) nil :: [] -(0)-> A(15, 13) nil :: [] -(0)-> A(7, 7) Cost-free Signatures used: -------------------------- #0 :: [] -(0)-> A_cf(0, 0) #EQ :: [] -(0)-> A_cf(0, 0) #EQ :: [] -(0)-> A_cf(14, 14) #GT :: [] -(0)-> A_cf(0, 0) #GT :: [] -(0)-> A_cf(14, 14) #LT :: [] -(0)-> A_cf(0, 0) #LT :: [] -(0)-> A_cf(14, 14) #cklt :: [A_cf(0, 0)] -(0)-> A_cf(11, 11) #cklt :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #compare :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 12) #compare :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #false :: [] -(0)-> A_cf(3, 3) #false :: [] -(0)-> A_cf(11, 11) #false :: [] -(0)-> A_cf(0, 0) #less :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(8, 8) #less :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #neg :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #pos :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #true :: [] -(0)-> A_cf(3, 3) #true :: [] -(0)-> A_cf(11, 11) #true :: [] -(0)-> A_cf(0, 0) :: :: [A_cf(0, 0) x A_cf(1, 0)] -(1)-> A_cf(1, 0) :: :: [A_cf(0, 0) x A_cf(5, 4)] -(1)-> A_cf(1, 4) :: :: [A_cf(0, 0) x A_cf(5, 0)] -(5)-> A_cf(5, 0) :: :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) findMin :: [A_cf(1, 0)] -(1)-> A_cf(1, 0) findMin :: [A_cf(5, 0)] -(1)-> A_cf(5, 0) findMin :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) findMin#1 :: [A_cf(1, 0)] -(1)-> A_cf(1, 0) findMin#1 :: [A_cf(5, 0)] -(1)-> A_cf(5, 0) findMin#1 :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) findMin#2 :: [A_cf(1, 0) x A_cf(0, 0)] -(1)-> A_cf(1, 0) findMin#2 :: [A_cf(5, 0) x A_cf(0, 0)] -(5)-> A_cf(5, 0) findMin#2 :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) findMin#3 :: [A_cf(3, 3) x A_cf(0, 0) x A_cf(0, 0) x A_cf(1, 0)] -(2)-> A_cf(1, 0) findMin#3 :: [A_cf(3, 3) x A_cf(0, 0) x A_cf(0, 0) x A_cf(5, 0)] -(10)-> A_cf(5, 0) findMin#3 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) minSort :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) minSort#1 :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) nil :: [] -(0)-> A_cf(1, 0) nil :: [] -(0)-> A_cf(15, 11) nil :: [] -(0)-> A_cf(3, 3) nil :: [] -(0)-> A_cf(5, 0) nil :: [] -(0)-> A_cf(11, 2) nil :: [] -(0)-> A_cf(0, 0) Base Constructor Signatures used: --------------------------------- #0_A :: [] -(0)-> A(0) #EQ_A :: [] -(0)-> A(0) #GT_A :: [] -(0)-> A(0) #LT_A :: [] -(0)-> A(0) #false_A :: [] -(0)-> A(0) #neg_A :: [A(0)] -(0)-> A(0) #pos_A :: [A(0)] -(0)-> A(0) #s_A :: [A(0)] -(0)-> A(0) #true_A :: [] -(0)-> A(0) ::_A :: [A(0) x A(0)] -(0)-> A(0) nil_A :: [] -(0)-> A(1, 0) nil_A :: [] -(0)-> A(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: findMin#1(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) 2. Weak: * 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))