* Step 1: Sum 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:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* 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))
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) = [6]
p(#GT) = [6]
p(#LT) = [6]
p(#cklt) = [1] x1 + [1]
p(#compare) = [6]
p(#false) = [7]
p(#less) = [0]
p(#neg) = [1] x1 + [0]
p(#pos) = [1] x1 + [0]
p(#s) = [1] x1 + [0]
p(#true) = [7]
p(::) = [1] x2 + [6]
p(findMin) = [1] x1 + [0]
p(findMin#1) = [1] x1 + [0]
p(findMin#2) = [1] x1 + [0]
p(findMin#3) = [1] x1 + [1] x4 + [0]
p(minSort) = [1] x1 + [0]
p(minSort#1) = [1] x1 + [1]
p(nil) = [0]
Following rules are strictly oriented:
findMin#1(::(@x,@xs)) = [1] @xs + [6]
> [1] @xs + [0]
= findMin#2(findMin(@xs),@x)
findMin#2(::(@y,@ys),@x) = [1] @ys + [6]
> [1] @ys + [0]
= findMin#3(#less(@x,@y),@x,@y,@ys)
minSort#1(::(@x,@xs)) = [1] @xs + [7]
> [1] @xs + [6]
= ::(@x,minSort(@xs))
minSort#1(nil()) = [1]
> [0]
= nil()
Following rules are (at-least) weakly oriented:
#cklt(#EQ()) = [7]
>= [7]
= #false()
#cklt(#GT()) = [7]
>= [7]
= #false()
#cklt(#LT()) = [7]
>= [7]
= #true()
#compare(#0(),#0()) = [6]
>= [6]
= #EQ()
#compare(#0(),#neg(@y)) = [6]
>= [6]
= #GT()
#compare(#0(),#pos(@y)) = [6]
>= [6]
= #LT()
#compare(#0(),#s(@y)) = [6]
>= [6]
= #LT()
#compare(#neg(@x),#0()) = [6]
>= [6]
= #LT()
#compare(#neg(@x),#neg(@y)) = [6]
>= [6]
= #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) = [6]
>= [6]
= #LT()
#compare(#pos(@x),#0()) = [6]
>= [6]
= #GT()
#compare(#pos(@x),#neg(@y)) = [6]
>= [6]
= #GT()
#compare(#pos(@x),#pos(@y)) = [6]
>= [6]
= #compare(@x,@y)
#compare(#s(@x),#0()) = [6]
>= [6]
= #GT()
#compare(#s(@x),#s(@y)) = [6]
>= [6]
= #compare(@x,@y)
#less(@x,@y) = [0]
>= [7]
= #cklt(#compare(@x,@y))
findMin(@l) = [1] @l + [0]
>= [1] @l + [0]
= findMin#1(@l)
findMin#1(nil()) = [0]
>= [0]
= nil()
findMin#2(nil(),@x) = [0]
>= [6]
= ::(@x,nil())
findMin#3(#false(),@x,@y,@ys) = [1] @ys + [7]
>= [1] @ys + [12]
= ::(@y,::(@x,@ys))
findMin#3(#true(),@x,@y,@ys) = [1] @ys + [7]
>= [1] @ys + [12]
= ::(@x,::(@y,@ys))
minSort(@l) = [1] @l + [0]
>= [1] @l + [1]
= minSort#1(findMin(@l))
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(@l) -> findMin#1(@l)
findMin#1(nil()) -> nil()
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))
- 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#1(::(@x,@xs)) -> findMin#2(findMin(@xs),@x)
findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@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) = [3]
p(#LT) = [0]
p(#cklt) = [1] x1 + [6]
p(#compare) = [3]
p(#false) = [0]
p(#less) = [0]
p(#neg) = [0]
p(#pos) = [1] x1 + [0]
p(#s) = [1] x1 + [0]
p(#true) = [1]
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) = [1] x1 + [0]
p(minSort#1) = [1] x1 + [0]
p(nil) = [1]
Following rules are strictly oriented:
findMin#3(#true(),@x,@y,@ys) = [1] @ys + [1]
> [1] @ys + [0]
= ::(@x,::(@y,@ys))
Following rules are (at-least) weakly oriented:
#cklt(#EQ()) = [6]
>= [0]
= #false()
#cklt(#GT()) = [9]
>= [0]
= #false()
#cklt(#LT()) = [6]
>= [1]
= #true()
#compare(#0(),#0()) = [3]
>= [0]
= #EQ()
#compare(#0(),#neg(@y)) = [3]
>= [3]
= #GT()
#compare(#0(),#pos(@y)) = [3]
>= [0]
= #LT()
#compare(#0(),#s(@y)) = [3]
>= [0]
= #LT()
#compare(#neg(@x),#0()) = [3]
>= [0]
= #LT()
#compare(#neg(@x),#neg(@y)) = [3]
>= [3]
= #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) = [3]
>= [0]
= #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]
>= [9]
= #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]
>= [1]
= nil()
findMin#2(::(@y,@ys),@x) = [1] @ys + [0]
>= [1] @ys + [0]
= findMin#3(#less(@x,@y),@x,@y,@ys)
findMin#2(nil(),@x) = [1]
>= [1]
= ::(@x,nil())
findMin#3(#false(),@x,@y,@ys) = [1] @ys + [0]
>= [1] @ys + [0]
= ::(@y,::(@x,@ys))
minSort(@l) = [1] @l + [0]
>= [0]
= minSort#1(findMin(@l))
minSort#1(::(@x,@xs)) = [1] @xs + [0]
>= [1] @xs + [0]
= ::(@x,minSort(@xs))
minSort#1(nil()) = [1]
>= [1]
= 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(@l) -> findMin#1(@l)
findMin#1(nil()) -> nil()
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#1(::(@x,@xs)) -> findMin#2(findMin(@xs),@x)
findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@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) = [1]
p(#GT) = [1]
p(#LT) = [0]
p(#cklt) = [1] x1 + [2]
p(#compare) = [2]
p(#false) = [1]
p(#less) = [0]
p(#neg) = [0]
p(#pos) = [1] x1 + [0]
p(#s) = [0]
p(#true) = [2]
p(::) = [1] x2 + [4]
p(findMin) = [1]
p(findMin#1) = [4]
p(findMin#2) = [1] x1 + [3]
p(findMin#3) = [1] x1 + [1] x4 + [7]
p(minSort) = [1] x1 + [0]
p(minSort#1) = [1] x1 + [0]
p(nil) = [0]
Following rules are strictly oriented:
findMin#1(nil()) = [4]
> [0]
= nil()
Following rules are (at-least) weakly oriented:
#cklt(#EQ()) = [3]
>= [1]
= #false()
#cklt(#GT()) = [3]
>= [1]
= #false()
#cklt(#LT()) = [2]
>= [2]
= #true()
#compare(#0(),#0()) = [2]
>= [1]
= #EQ()
#compare(#0(),#neg(@y)) = [2]
>= [1]
= #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]
>= [1]
= #GT()
#compare(#pos(@x),#neg(@y)) = [2]
>= [1]
= #GT()
#compare(#pos(@x),#pos(@y)) = [2]
>= [2]
= #compare(@x,@y)
#compare(#s(@x),#0()) = [2]
>= [1]
= #GT()
#compare(#s(@x),#s(@y)) = [2]
>= [2]
= #compare(@x,@y)
#less(@x,@y) = [0]
>= [4]
= #cklt(#compare(@x,@y))
findMin(@l) = [1]
>= [4]
= findMin#1(@l)
findMin#1(::(@x,@xs)) = [4]
>= [4]
= findMin#2(findMin(@xs),@x)
findMin#2(::(@y,@ys),@x) = [1] @ys + [7]
>= [1] @ys + [7]
= findMin#3(#less(@x,@y),@x,@y,@ys)
findMin#2(nil(),@x) = [3]
>= [4]
= ::(@x,nil())
findMin#3(#false(),@x,@y,@ys) = [1] @ys + [8]
>= [1] @ys + [8]
= ::(@y,::(@x,@ys))
findMin#3(#true(),@x,@y,@ys) = [1] @ys + [9]
>= [1] @ys + [8]
= ::(@x,::(@y,@ys))
minSort(@l) = [1] @l + [0]
>= [1]
= 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 5: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
#less(@x,@y) -> #cklt(#compare(@x,@y))
findMin(@l) -> findMin#1(@l)
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#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#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) = [1]
p(#LT) = [1]
p(#cklt) = [1] x1 + [2]
p(#compare) = [5]
p(#false) = [3]
p(#less) = [1]
p(#neg) = [0]
p(#pos) = [1] x1 + [0]
p(#s) = [1] x1 + [0]
p(#true) = [0]
p(::) = [1] x2 + [0]
p(findMin) = [1]
p(findMin#1) = [3]
p(findMin#2) = [1] x1 + [1]
p(findMin#3) = [1] x1 + [1] x4 + [0]
p(minSort) = [1]
p(minSort#1) = [1] x1 + [1]
p(nil) = [0]
Following rules are strictly oriented:
findMin#2(nil(),@x) = [1]
> [0]
= ::(@x,nil())
findMin#3(#false(),@x,@y,@ys) = [1] @ys + [3]
> [1] @ys + [0]
= ::(@y,::(@x,@ys))
Following rules are (at-least) weakly oriented:
#cklt(#EQ()) = [4]
>= [3]
= #false()
#cklt(#GT()) = [3]
>= [3]
= #false()
#cklt(#LT()) = [3]
>= [0]
= #true()
#compare(#0(),#0()) = [5]
>= [2]
= #EQ()
#compare(#0(),#neg(@y)) = [5]
>= [1]
= #GT()
#compare(#0(),#pos(@y)) = [5]
>= [1]
= #LT()
#compare(#0(),#s(@y)) = [5]
>= [1]
= #LT()
#compare(#neg(@x),#0()) = [5]
>= [1]
= #LT()
#compare(#neg(@x),#neg(@y)) = [5]
>= [5]
= #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) = [5]
>= [1]
= #LT()
#compare(#pos(@x),#0()) = [5]
>= [1]
= #GT()
#compare(#pos(@x),#neg(@y)) = [5]
>= [1]
= #GT()
#compare(#pos(@x),#pos(@y)) = [5]
>= [5]
= #compare(@x,@y)
#compare(#s(@x),#0()) = [5]
>= [1]
= #GT()
#compare(#s(@x),#s(@y)) = [5]
>= [5]
= #compare(@x,@y)
#less(@x,@y) = [1]
>= [7]
= #cklt(#compare(@x,@y))
findMin(@l) = [1]
>= [3]
= findMin#1(@l)
findMin#1(::(@x,@xs)) = [3]
>= [2]
= findMin#2(findMin(@xs),@x)
findMin#1(nil()) = [3]
>= [0]
= nil()
findMin#2(::(@y,@ys),@x) = [1] @ys + [1]
>= [1] @ys + [1]
= findMin#3(#less(@x,@y),@x,@y,@ys)
findMin#3(#true(),@x,@y,@ys) = [1] @ys + [0]
>= [1] @ys + [0]
= ::(@x,::(@y,@ys))
minSort(@l) = [1]
>= [2]
= minSort#1(findMin(@l))
minSort#1(::(@x,@xs)) = [1] @xs + [1]
>= [1]
= ::(@x,minSort(@xs))
minSort#1(nil()) = [1]
>= [0]
= nil()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
#less(@x,@y) -> #cklt(#compare(@x,@y))
findMin(@l) -> findMin#1(@l)
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#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#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) = [0]
p(#LT) = [0]
p(#cklt) = [1] x1 + [3]
p(#compare) = [0]
p(#false) = [0]
p(#less) = [4]
p(#neg) = [0]
p(#pos) = [0]
p(#s) = [1] x1 + [0]
p(#true) = [0]
p(::) = [1] x2 + [0]
p(findMin) = [0]
p(findMin#1) = [4]
p(findMin#2) = [1] x1 + [4]
p(findMin#3) = [1] x1 + [1] x4 + [0]
p(minSort) = [1] x1 + [0]
p(minSort#1) = [1] x1 + [0]
p(nil) = [4]
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()) = [3]
>= [0]
= #false()
#cklt(#LT()) = [3]
>= [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)
findMin(@l) = [0]
>= [4]
= findMin#1(@l)
findMin#1(::(@x,@xs)) = [4]
>= [4]
= findMin#2(findMin(@xs),@x)
findMin#1(nil()) = [4]
>= [4]
= nil()
findMin#2(::(@y,@ys),@x) = [1] @ys + [4]
>= [1] @ys + [4]
= findMin#3(#less(@x,@y),@x,@y,@ys)
findMin#2(nil(),@x) = [8]
>= [4]
= ::(@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]
>= [0]
= minSort#1(findMin(@l))
minSort#1(::(@x,@xs)) = [1] @xs + [0]
>= [1] @xs + [0]
= ::(@x,minSort(@xs))
minSort#1(nil()) = [4]
>= [4]
= nil()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 7: MI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
findMin(@l) -> findMin#1(@l)
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#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#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:
MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 1, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
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) = [8]
p(#EQ) = [0]
p(#GT) = [0]
p(#LT) = [0]
p(#cklt) = [1] x_1 + [0]
p(#compare) = [0]
p(#false) = [0]
p(#less) = [0]
p(#neg) = [1] x_1 + [0]
p(#pos) = [4]
p(#s) = [1] x_1 + [0]
p(#true) = [0]
p(::) = [1] x_2 + [1]
p(findMin) = [1] x_1 + [0]
p(findMin#1) = [1] x_1 + [0]
p(findMin#2) = [1] x_1 + [1]
p(findMin#3) = [4] x_1 + [1] x_4 + [2]
p(minSort) = [2] x_1 + [10]
p(minSort#1) = [2] x_1 + [9]
p(nil) = [0]
Following rules are strictly oriented:
minSort(@l) = [2] @l + [10]
> [2] @l + [9]
= 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)) = [2] @xs + [11]
>= [2] @xs + [11]
= ::(@x,minSort(@xs))
minSort#1(nil()) = [9]
>= [0]
= nil()
* Step 8: MI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
findMin(@l) -> findMin#1(@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#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:
MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
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]
[1]
p(#GT) = [1]
[1]
p(#LT) = [1]
[1]
p(#cklt) = [4 0] x_1 + [0]
[0 2] [0]
p(#compare) = [1]
[1]
p(#false) = [2]
[2]
p(#less) = [4]
[2]
p(#neg) = [0]
[0]
p(#pos) = [0 0] x_1 + [0]
[0 1] [1]
p(#s) = [0]
[0]
p(#true) = [3]
[2]
p(::) = [0 1] x_1 + [1 2] x_2 + [0]
[0 0] [0 1] [5]
p(findMin) = [1 1] x_1 + [2]
[0 1] [0]
p(findMin#1) = [1 1] x_1 + [0]
[0 1] [0]
p(findMin#2) = [1 2] x_1 + [0 1] x_2 + [2]
[0 1] [0 0] [5]
p(findMin#3) = [1 4] x_1 + [0 1] x_2 + [0 1] x_3 + [1 4] x_4 + [0]
[0 4] [0 0] [0 0] [0 1] [2]
p(minSort) = [2 3] x_1 + [6]
[0 1] [0]
p(minSort#1) = [2 1] x_1 + [1]
[0 1] [0]
p(nil) = [0]
[0]
Following rules are strictly oriented:
findMin(@l) = [1 1] @l + [2]
[0 1] [0]
> [1 1] @l + [0]
[0 1] [0]
= findMin#1(@l)
Following rules are (at-least) weakly oriented:
#cklt(#EQ()) = [4]
[2]
>= [2]
[2]
= #false()
#cklt(#GT()) = [4]
[2]
>= [2]
[2]
= #false()
#cklt(#LT()) = [4]
[2]
>= [3]
[2]
= #true()
#compare(#0(),#0()) = [1]
[1]
>= [1]
[1]
= #EQ()
#compare(#0(),#neg(@y)) = [1]
[1]
>= [1]
[1]
= #GT()
#compare(#0(),#pos(@y)) = [1]
[1]
>= [1]
[1]
= #LT()
#compare(#0(),#s(@y)) = [1]
[1]
>= [1]
[1]
= #LT()
#compare(#neg(@x),#0()) = [1]
[1]
>= [1]
[1]
= #LT()
#compare(#neg(@x),#neg(@y)) = [1]
[1]
>= [1]
[1]
= #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) = [1]
[1]
>= [1]
[1]
= #LT()
#compare(#pos(@x),#0()) = [1]
[1]
>= [1]
[1]
= #GT()
#compare(#pos(@x),#neg(@y)) = [1]
[1]
>= [1]
[1]
= #GT()
#compare(#pos(@x),#pos(@y)) = [1]
[1]
>= [1]
[1]
= #compare(@x,@y)
#compare(#s(@x),#0()) = [1]
[1]
>= [1]
[1]
= #GT()
#compare(#s(@x),#s(@y)) = [1]
[1]
>= [1]
[1]
= #compare(@x,@y)
#less(@x,@y) = [4]
[2]
>= [4]
[2]
= #cklt(#compare(@x,@y))
findMin#1(::(@x,@xs)) = [0 1] @x + [1 3] @xs + [5]
[0 0] [0 1] [5]
>= [0 1] @x + [1 3] @xs + [4]
[0 0] [0 1] [5]
= findMin#2(findMin(@xs),@x)
findMin#1(nil()) = [0]
[0]
>= [0]
[0]
= nil()
findMin#2(::(@y,@ys),@x) = [0 1] @x + [0 1] @y + [1 4] @ys + [12]
[0 0] [0 0] [0 1] [10]
>= [0 1] @x + [0 1] @y + [1 4] @ys + [12]
[0 0] [0 0] [0 1] [10]
= findMin#3(#less(@x,@y),@x,@y,@ys)
findMin#2(nil(),@x) = [0 1] @x + [2]
[0 0] [5]
>= [0 1] @x + [0]
[0 0] [5]
= ::(@x,nil())
findMin#3(#false(),@x,@y,@ys) = [0 1] @x + [0 1] @y + [1 4] @ys + [10]
[0 0] [0 0] [0 1] [10]
>= [0 1] @x + [0 1] @y + [1 4] @ys + [10]
[0 0] [0 0] [0 1] [10]
= ::(@y,::(@x,@ys))
findMin#3(#true(),@x,@y,@ys) = [0 1] @x + [0 1] @y + [1 4] @ys + [11]
[0 0] [0 0] [0 1] [10]
>= [0 1] @x + [0 1] @y + [1 4] @ys + [10]
[0 0] [0 0] [0 1] [10]
= ::(@x,::(@y,@ys))
minSort(@l) = [2 3] @l + [6]
[0 1] [0]
>= [2 3] @l + [5]
[0 1] [0]
= minSort#1(findMin(@l))
minSort#1(::(@x,@xs)) = [0 2] @x + [2 5] @xs + [6]
[0 0] [0 1] [5]
>= [0 1] @x + [2 5] @xs + [6]
[0 0] [0 1] [5]
= ::(@x,minSort(@xs))
minSort#1(nil()) = [1]
[0]
>= [0]
[0]
= nil()
* Step 9: 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))