*** 1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
#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 DP Rules:
Weak TRS Rules:
#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
basic terms: {#cklt,#compare,#less,findMin,findMin#1,findMin#2,findMin#3,minSort,minSort#1}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
#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 DP Rules:
Weak TRS Rules:
#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
basic terms: {#cklt,#compare,#less,findMin,findMin#1,findMin#2,findMin#3,minSort,minSort#1}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
#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 DP Rules:
Weak TRS Rules:
#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
basic terms: {#cklt,#compare,#less,findMin,findMin#1,findMin#2,findMin#3,minSort,minSort#1}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
#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 DP Rules:
Weak TRS Rules:
#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
basic terms: {#cklt,#compare,#less,findMin,findMin#1,findMin#2,findMin#3,minSort,minSort#1}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
#less(@x,@y) -> #cklt(#compare(@x,@y))
findMin(@l) -> findMin#1(@l)
minSort(@l) -> minSort#1(findMin(@l))
Weak DP Rules:
Weak TRS Rules:
#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
basic terms: {#cklt,#compare,#less,findMin,findMin#1,findMin#2,findMin#3,minSort,minSort#1}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
findMin(@l) -> findMin#1(@l)
minSort(@l) -> minSort#1(findMin(@l))
Weak DP Rules:
Weak TRS Rules:
#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
basic terms: {#cklt,#compare,#less,findMin,findMin#1,findMin#2,findMin#3,minSort,minSort#1}/{#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, greedy = NoGreedy}
Proof:
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) = [2]
p(#EQ) = [0]
p(#GT) = [0]
p(#LT) = [0]
p(#cklt) = [2] x1 + [0]
p(#compare) = [0]
p(#false) = [0]
p(#less) = [0]
p(#neg) = [0]
p(#pos) = [0]
p(#s) = [0]
p(#true) = [0]
p(::) = [1] x2 + [2]
p(findMin) = [1] x1 + [0]
p(findMin#1) = [1] x1 + [0]
p(findMin#2) = [1] x1 + [2]
p(findMin#3) = [2] x1 + [1] x4 + [4]
p(minSort) = [3] x1 + [4]
p(minSort#1) = [3] x1 + [0]
p(nil) = [0]
Following rules are strictly oriented:
minSort(@l) = [3] @l + [4]
> [3] @l + [0]
= 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 + [2]
>= [1] @xs + [2]
= findMin#2(findMin(@xs),@x)
findMin#1(nil()) = [0]
>= [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) = [2]
>= [2]
= ::(@x,nil())
findMin#3(#false(),@x,@y,@ys) = [1] @ys + [4]
>= [1] @ys + [4]
= ::(@y,::(@x,@ys))
findMin#3(#true(),@x,@y,@ys) = [1] @ys + [4]
>= [1] @ys + [4]
= ::(@x,::(@y,@ys))
minSort#1(::(@x,@xs)) = [3] @xs + [6]
>= [3] @xs + [6]
= ::(@x,minSort(@xs))
minSort#1(nil()) = [0]
>= [0]
= nil()
*** 1.1.1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
findMin(@l) -> findMin#1(@l)
Weak DP Rules:
Weak TRS Rules:
#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
basic terms: {#cklt,#compare,#less,findMin,findMin#1,findMin#2,findMin#3,minSort,minSort#1}/{#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, greedy = NoGreedy}
Proof:
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) = [0]
[0]
p(#GT) = [0]
[0]
p(#LT) = [0]
[0]
p(#cklt) = [1 0] x1 + [1]
[0 0] [1]
p(#compare) = [1]
[0]
p(#false) = [1]
[1]
p(#less) = [2]
[1]
p(#neg) = [0]
[0]
p(#pos) = [0 1] x1 + [0]
[0 1] [1]
p(#s) = [0 4] x1 + [0]
[0 1] [0]
p(#true) = [1]
[1]
p(::) = [1 3] x2 + [0]
[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 + [4]
[0 1] [3]
p(findMin#3) = [4 4] x1 + [1 6] x4 + [1]
[0 6] [0 1] [0]
p(minSort) = [3 7] x1 + [3]
[0 1] [0]
p(minSort#1) = [3 1] x1 + [0]
[0 1] [0]
p(nil) = [2]
[0]
Following rules are strictly oriented:
findMin(@l) = [1 2] @l + [1]
[0 1] [0]
> [1 2] @l + [0]
[0 1] [0]
= findMin#1(@l)
Following rules are (at-least) weakly oriented:
#cklt(#EQ()) = [1]
[1]
>= [1]
[1]
= #false()
#cklt(#GT()) = [1]
[1]
>= [1]
[1]
= #false()
#cklt(#LT()) = [1]
[1]
>= [1]
[1]
= #true()
#compare(#0(),#0()) = [1]
[0]
>= [0]
[0]
= #EQ()
#compare(#0(),#neg(@y)) = [1]
[0]
>= [0]
[0]
= #GT()
#compare(#0(),#pos(@y)) = [1]
[0]
>= [0]
[0]
= #LT()
#compare(#0(),#s(@y)) = [1]
[0]
>= [0]
[0]
= #LT()
#compare(#neg(@x),#0()) = [1]
[0]
>= [0]
[0]
= #LT()
#compare(#neg(@x),#neg(@y)) = [1]
[0]
>= [1]
[0]
= #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) = [1]
[0]
>= [0]
[0]
= #LT()
#compare(#pos(@x),#0()) = [1]
[0]
>= [0]
[0]
= #GT()
#compare(#pos(@x),#neg(@y)) = [1]
[0]
>= [0]
[0]
= #GT()
#compare(#pos(@x),#pos(@y)) = [1]
[0]
>= [1]
[0]
= #compare(@x,@y)
#compare(#s(@x),#0()) = [1]
[0]
>= [0]
[0]
= #GT()
#compare(#s(@x),#s(@y)) = [1]
[0]
>= [1]
[0]
= #compare(@x,@y)
#less(@x,@y) = [2]
[1]
>= [2]
[1]
= #cklt(#compare(@x,@y))
findMin#1(::(@x,@xs)) = [1 5] @xs + [6]
[0 1] [3]
>= [1 5] @xs + [5]
[0 1] [3]
= findMin#2(findMin(@xs),@x)
findMin#1(nil()) = [2]
[0]
>= [2]
[0]
= nil()
findMin#2(::(@y,@ys),@x) = [1 6] @ys + [13]
[0 1] [6]
>= [1 6] @ys + [13]
[0 1] [6]
= findMin#3(#less(@x,@y)
,@x
,@y
,@ys)
findMin#2(nil(),@x) = [6]
[3]
>= [2]
[3]
= ::(@x,nil())
findMin#3(#false(),@x,@y,@ys) = [1 6] @ys + [9]
[0 1] [6]
>= [1 6] @ys + [9]
[0 1] [6]
= ::(@y,::(@x,@ys))
findMin#3(#true(),@x,@y,@ys) = [1 6] @ys + [9]
[0 1] [6]
>= [1 6] @ys + [9]
[0 1] [6]
= ::(@x,::(@y,@ys))
minSort(@l) = [3 7] @l + [3]
[0 1] [0]
>= [3 7] @l + [3]
[0 1] [0]
= minSort#1(findMin(@l))
minSort#1(::(@x,@xs)) = [3 10] @xs + [3]
[0 1] [3]
>= [3 10] @xs + [3]
[0 1] [3]
= ::(@x,minSort(@xs))
minSort#1(nil()) = [6]
[0]
>= [2]
[0]
= nil()
*** 1.1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#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
basic terms: {#cklt,#compare,#less,findMin,findMin#1,findMin#2,findMin#3,minSort,minSort#1}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).