We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
, minSort#1(nil()) -> nil()
, findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
, findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
, findMin#1(nil()) -> nil()
, findMin(@l) -> findMin#1(@l)
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, minSort(@l) -> minSort#1(findMin(@l))
, findMin#2(::(@y, @ys), @x) ->
findMin#3(#less(@x, @y), @x, @y, @ys)
, findMin#2(nil(), @x) -> ::(@x, nil()) }
Weak Trs:
{ #cklt(#LT()) -> #true()
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
Uargs(#cklt) = {1}, Uargs(findMin#2) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[minSort#1](x1) = [1] x1 + [0]
[#true] = [1]
[#false] = [0]
[findMin#3](x1, x2, x3, x4) = [1] x1 + [1] x4 + [0]
[::](x1, x2) = [1] x2 + [0]
[#LT] = [1]
[findMin#1](x1) = [0]
[#cklt](x1) = [1] x1 + [0]
[#pos](x1) = [1] x1 + [0]
[#0] = [0]
[findMin](x1) = [0]
[#neg](x1) = [1] x1 + [0]
[#EQ] = [0]
[#less](x1, x2) = [0]
[minSort](x1) = [1] x1 + [0]
[#compare](x1, x2) = [4]
[#s](x1) = [1] x1 + [0]
[#GT] = [0]
[nil] = [0]
[findMin#2](x1, x2) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[minSort#1(::(@x, @xs))] = [1] @xs + [0]
>= [1] @xs + [0]
= [::(@x, minSort(@xs))]
[minSort#1(nil())] = [0]
>= [0]
= [nil()]
[findMin#3(#true(), @x, @y, @ys)] = [1] @ys + [1]
> [1] @ys + [0]
= [::(@x, ::(@y, @ys))]
[findMin#3(#false(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@y, ::(@x, @ys))]
[findMin#1(::(@x, @xs))] = [0]
>= [0]
= [findMin#2(findMin(@xs), @x)]
[findMin#1(nil())] = [0]
>= [0]
= [nil()]
[#cklt(#LT())] = [1]
>= [1]
= [#true()]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[findMin(@l)] = [0]
>= [0]
= [findMin#1(@l)]
[#less(@x, @y)] = [0]
? [4]
= [#cklt(#compare(@x, @y))]
[minSort(@l)] = [1] @l + [0]
>= [0]
= [minSort#1(findMin(@l))]
[#compare(#pos(@x), #pos(@y))] = [4]
>= [4]
= [#compare(@x, @y)]
[#compare(#pos(@x), #0())] = [4]
> [0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [4]
> [0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [4]
> [1]
= [#LT()]
[#compare(#0(), #0())] = [4]
> [0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [4]
> [0]
= [#GT()]
[#compare(#0(), #s(@y))] = [4]
> [1]
= [#LT()]
[#compare(#neg(@x), #pos(@y))] = [4]
> [1]
= [#LT()]
[#compare(#neg(@x), #0())] = [4]
> [1]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [4]
>= [4]
= [#compare(@y, @x)]
[#compare(#s(@x), #0())] = [4]
> [0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [4]
>= [4]
= [#compare(@x, @y)]
[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())]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
, minSort#1(nil()) -> nil()
, findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
, findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
, findMin#1(nil()) -> nil()
, findMin(@l) -> findMin#1(@l)
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, minSort(@l) -> minSort#1(findMin(@l))
, findMin#2(::(@y, @ys), @x) ->
findMin#3(#less(@x, @y), @x, @y, @ys)
, findMin#2(nil(), @x) -> ::(@x, nil()) }
Weak Trs:
{ findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, #cklt(#LT()) -> #true()
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
Uargs(#cklt) = {1}, Uargs(findMin#2) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[minSort#1](x1) = [1] x1 + [0]
[#true] = [0]
[#false] = [1]
[findMin#3](x1, x2, x3, x4) = [1] x1 + [1] x4 + [0]
[::](x1, x2) = [1] x2 + [0]
[#LT] = [0]
[findMin#1](x1) = [0]
[#cklt](x1) = [1] x1 + [0]
[#pos](x1) = [1] x1 + [0]
[#0] = [0]
[findMin](x1) = [0]
[#neg](x1) = [1] x1 + [0]
[#EQ] = [1]
[#less](x1, x2) = [0]
[minSort](x1) = [1] x1 + [0]
[#compare](x1, x2) = [4]
[#s](x1) = [1] x1 + [0]
[#GT] = [1]
[nil] = [0]
[findMin#2](x1, x2) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[minSort#1(::(@x, @xs))] = [1] @xs + [0]
>= [1] @xs + [0]
= [::(@x, minSort(@xs))]
[minSort#1(nil())] = [0]
>= [0]
= [nil()]
[findMin#3(#true(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@x, ::(@y, @ys))]
[findMin#3(#false(), @x, @y, @ys)] = [1] @ys + [1]
> [1] @ys + [0]
= [::(@y, ::(@x, @ys))]
[findMin#1(::(@x, @xs))] = [0]
>= [0]
= [findMin#2(findMin(@xs), @x)]
[findMin#1(nil())] = [0]
>= [0]
= [nil()]
[#cklt(#LT())] = [0]
>= [0]
= [#true()]
[#cklt(#EQ())] = [1]
>= [1]
= [#false()]
[#cklt(#GT())] = [1]
>= [1]
= [#false()]
[findMin(@l)] = [0]
>= [0]
= [findMin#1(@l)]
[#less(@x, @y)] = [0]
? [4]
= [#cklt(#compare(@x, @y))]
[minSort(@l)] = [1] @l + [0]
>= [0]
= [minSort#1(findMin(@l))]
[#compare(#pos(@x), #pos(@y))] = [4]
>= [4]
= [#compare(@x, @y)]
[#compare(#pos(@x), #0())] = [4]
> [1]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [4]
> [1]
= [#GT()]
[#compare(#0(), #pos(@y))] = [4]
> [0]
= [#LT()]
[#compare(#0(), #0())] = [4]
> [1]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [4]
> [1]
= [#GT()]
[#compare(#0(), #s(@y))] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #pos(@y))] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #0())] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [4]
>= [4]
= [#compare(@y, @x)]
[#compare(#s(@x), #0())] = [4]
> [1]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [4]
>= [4]
= [#compare(@x, @y)]
[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())]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
, minSort#1(nil()) -> nil()
, findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
, findMin#1(nil()) -> nil()
, findMin(@l) -> findMin#1(@l)
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, minSort(@l) -> minSort#1(findMin(@l))
, findMin#2(::(@y, @ys), @x) ->
findMin#3(#less(@x, @y), @x, @y, @ys)
, findMin#2(nil(), @x) -> ::(@x, nil()) }
Weak Trs:
{ findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
, #cklt(#LT()) -> #true()
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
Uargs(#cklt) = {1}, Uargs(findMin#2) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[minSort#1](x1) = [1] x1 + [0]
[#true] = [0]
[#false] = [0]
[findMin#3](x1, x2, x3, x4) = [1] x1 + [1] x4 + [0]
[::](x1, x2) = [1] x2 + [0]
[#LT] = [0]
[findMin#1](x1) = [1] x1 + [0]
[#cklt](x1) = [1] x1 + [0]
[#pos](x1) = [1] x1 + [0]
[#0] = [0]
[findMin](x1) = [1] x1 + [4]
[#neg](x1) = [1] x1 + [0]
[#EQ] = [0]
[#less](x1, x2) = [0]
[minSort](x1) = [1] x1 + [0]
[#compare](x1, x2) = [4]
[#s](x1) = [1] x1 + [0]
[#GT] = [0]
[nil] = [1]
[findMin#2](x1, x2) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[minSort#1(::(@x, @xs))] = [1] @xs + [0]
>= [1] @xs + [0]
= [::(@x, minSort(@xs))]
[minSort#1(nil())] = [1]
>= [1]
= [nil()]
[findMin#3(#true(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@x, ::(@y, @ys))]
[findMin#3(#false(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@y, ::(@x, @ys))]
[findMin#1(::(@x, @xs))] = [1] @xs + [0]
? [1] @xs + [4]
= [findMin#2(findMin(@xs), @x)]
[findMin#1(nil())] = [1]
>= [1]
= [nil()]
[#cklt(#LT())] = [0]
>= [0]
= [#true()]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[findMin(@l)] = [1] @l + [4]
> [1] @l + [0]
= [findMin#1(@l)]
[#less(@x, @y)] = [0]
? [4]
= [#cklt(#compare(@x, @y))]
[minSort(@l)] = [1] @l + [0]
? [1] @l + [4]
= [minSort#1(findMin(@l))]
[#compare(#pos(@x), #pos(@y))] = [4]
>= [4]
= [#compare(@x, @y)]
[#compare(#pos(@x), #0())] = [4]
> [0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [4]
> [0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [4]
> [0]
= [#LT()]
[#compare(#0(), #0())] = [4]
> [0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [4]
> [0]
= [#GT()]
[#compare(#0(), #s(@y))] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #pos(@y))] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #0())] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [4]
>= [4]
= [#compare(@y, @x)]
[#compare(#s(@x), #0())] = [4]
> [0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [4]
>= [4]
= [#compare(@x, @y)]
[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())]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
, minSort#1(nil()) -> nil()
, findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
, findMin#1(nil()) -> nil()
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, minSort(@l) -> minSort#1(findMin(@l))
, findMin#2(::(@y, @ys), @x) ->
findMin#3(#less(@x, @y), @x, @y, @ys)
, findMin#2(nil(), @x) -> ::(@x, nil()) }
Weak Trs:
{ findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
, #cklt(#LT()) -> #true()
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, findMin(@l) -> findMin#1(@l)
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
Uargs(#cklt) = {1}, Uargs(findMin#2) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[minSort#1](x1) = [1] x1 + [0]
[#true] = [0]
[#false] = [0]
[findMin#3](x1, x2, x3, x4) = [1] x1 + [1] x4 + [0]
[::](x1, x2) = [1] x2 + [0]
[#LT] = [0]
[findMin#1](x1) = [1] x1 + [0]
[#cklt](x1) = [1] x1 + [0]
[#pos](x1) = [1] x1 + [0]
[#0] = [0]
[findMin](x1) = [1] x1 + [0]
[#neg](x1) = [1] x1 + [0]
[#EQ] = [0]
[#less](x1, x2) = [0]
[minSort](x1) = [1] x1 + [1]
[#compare](x1, x2) = [4]
[#s](x1) = [1] x1 + [0]
[#GT] = [0]
[nil] = [1]
[findMin#2](x1, x2) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[minSort#1(::(@x, @xs))] = [1] @xs + [0]
? [1] @xs + [1]
= [::(@x, minSort(@xs))]
[minSort#1(nil())] = [1]
>= [1]
= [nil()]
[findMin#3(#true(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@x, ::(@y, @ys))]
[findMin#3(#false(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@y, ::(@x, @ys))]
[findMin#1(::(@x, @xs))] = [1] @xs + [0]
>= [1] @xs + [0]
= [findMin#2(findMin(@xs), @x)]
[findMin#1(nil())] = [1]
>= [1]
= [nil()]
[#cklt(#LT())] = [0]
>= [0]
= [#true()]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[findMin(@l)] = [1] @l + [0]
>= [1] @l + [0]
= [findMin#1(@l)]
[#less(@x, @y)] = [0]
? [4]
= [#cklt(#compare(@x, @y))]
[minSort(@l)] = [1] @l + [1]
> [1] @l + [0]
= [minSort#1(findMin(@l))]
[#compare(#pos(@x), #pos(@y))] = [4]
>= [4]
= [#compare(@x, @y)]
[#compare(#pos(@x), #0())] = [4]
> [0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [4]
> [0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [4]
> [0]
= [#LT()]
[#compare(#0(), #0())] = [4]
> [0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [4]
> [0]
= [#GT()]
[#compare(#0(), #s(@y))] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #pos(@y))] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #0())] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [4]
>= [4]
= [#compare(@y, @x)]
[#compare(#s(@x), #0())] = [4]
> [0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [4]
>= [4]
= [#compare(@x, @y)]
[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())]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
, minSort#1(nil()) -> nil()
, findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
, findMin#1(nil()) -> nil()
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, findMin#2(::(@y, @ys), @x) ->
findMin#3(#less(@x, @y), @x, @y, @ys)
, findMin#2(nil(), @x) -> ::(@x, nil()) }
Weak Trs:
{ findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
, #cklt(#LT()) -> #true()
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, findMin(@l) -> findMin#1(@l)
, minSort(@l) -> minSort#1(findMin(@l))
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
Uargs(#cklt) = {1}, Uargs(findMin#2) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[minSort#1](x1) = [1] x1 + [0]
[#true] = [0]
[#false] = [0]
[findMin#3](x1, x2, x3, x4) = [1] x1 + [1] x4 + [0]
[::](x1, x2) = [1] x2 + [0]
[#LT] = [0]
[findMin#1](x1) = [1] x1 + [0]
[#cklt](x1) = [1] x1 + [0]
[#pos](x1) = [1] x1 + [0]
[#0] = [0]
[findMin](x1) = [1] x1 + [0]
[#neg](x1) = [1] x1 + [0]
[#EQ] = [0]
[#less](x1, x2) = [5]
[minSort](x1) = [1] x1 + [4]
[#compare](x1, x2) = [4]
[#s](x1) = [1] x1 + [0]
[#GT] = [0]
[nil] = [1]
[findMin#2](x1, x2) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[minSort#1(::(@x, @xs))] = [1] @xs + [0]
? [1] @xs + [4]
= [::(@x, minSort(@xs))]
[minSort#1(nil())] = [1]
>= [1]
= [nil()]
[findMin#3(#true(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@x, ::(@y, @ys))]
[findMin#3(#false(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@y, ::(@x, @ys))]
[findMin#1(::(@x, @xs))] = [1] @xs + [0]
>= [1] @xs + [0]
= [findMin#2(findMin(@xs), @x)]
[findMin#1(nil())] = [1]
>= [1]
= [nil()]
[#cklt(#LT())] = [0]
>= [0]
= [#true()]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[findMin(@l)] = [1] @l + [0]
>= [1] @l + [0]
= [findMin#1(@l)]
[#less(@x, @y)] = [5]
> [4]
= [#cklt(#compare(@x, @y))]
[minSort(@l)] = [1] @l + [4]
> [1] @l + [0]
= [minSort#1(findMin(@l))]
[#compare(#pos(@x), #pos(@y))] = [4]
>= [4]
= [#compare(@x, @y)]
[#compare(#pos(@x), #0())] = [4]
> [0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [4]
> [0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [4]
> [0]
= [#LT()]
[#compare(#0(), #0())] = [4]
> [0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [4]
> [0]
= [#GT()]
[#compare(#0(), #s(@y))] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #pos(@y))] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #0())] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [4]
>= [4]
= [#compare(@y, @x)]
[#compare(#s(@x), #0())] = [4]
> [0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [4]
>= [4]
= [#compare(@x, @y)]
[findMin#2(::(@y, @ys), @x)] = [1] @ys + [0]
? [1] @ys + [5]
= [findMin#3(#less(@x, @y), @x, @y, @ys)]
[findMin#2(nil(), @x)] = [1]
>= [1]
= [::(@x, nil())]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
, minSort#1(nil()) -> nil()
, 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()) }
Weak Trs:
{ findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
, #cklt(#LT()) -> #true()
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, findMin(@l) -> findMin#1(@l)
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, minSort(@l) -> minSort#1(findMin(@l))
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
Uargs(#cklt) = {1}, Uargs(findMin#2) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[minSort#1](x1) = [1] x1 + [0]
[#true] = [0]
[#false] = [0]
[findMin#3](x1, x2, x3, x4) = [1] x1 + [1] x4 + [0]
[::](x1, x2) = [1] x2 + [0]
[#LT] = [0]
[findMin#1](x1) = [1]
[#cklt](x1) = [1] x1 + [0]
[#pos](x1) = [1] x1 + [0]
[#0] = [0]
[findMin](x1) = [1]
[#neg](x1) = [1] x1 + [0]
[#EQ] = [0]
[#less](x1, x2) = [4]
[minSort](x1) = [1] x1 + [1]
[#compare](x1, x2) = [4]
[#s](x1) = [1] x1 + [0]
[#GT] = [0]
[nil] = [0]
[findMin#2](x1, x2) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[minSort#1(::(@x, @xs))] = [1] @xs + [0]
? [1] @xs + [1]
= [::(@x, minSort(@xs))]
[minSort#1(nil())] = [0]
>= [0]
= [nil()]
[findMin#3(#true(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@x, ::(@y, @ys))]
[findMin#3(#false(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@y, ::(@x, @ys))]
[findMin#1(::(@x, @xs))] = [1]
>= [1]
= [findMin#2(findMin(@xs), @x)]
[findMin#1(nil())] = [1]
> [0]
= [nil()]
[#cklt(#LT())] = [0]
>= [0]
= [#true()]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[findMin(@l)] = [1]
>= [1]
= [findMin#1(@l)]
[#less(@x, @y)] = [4]
>= [4]
= [#cklt(#compare(@x, @y))]
[minSort(@l)] = [1] @l + [1]
>= [1]
= [minSort#1(findMin(@l))]
[#compare(#pos(@x), #pos(@y))] = [4]
>= [4]
= [#compare(@x, @y)]
[#compare(#pos(@x), #0())] = [4]
> [0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [4]
> [0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [4]
> [0]
= [#LT()]
[#compare(#0(), #0())] = [4]
> [0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [4]
> [0]
= [#GT()]
[#compare(#0(), #s(@y))] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #pos(@y))] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #0())] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [4]
>= [4]
= [#compare(@y, @x)]
[#compare(#s(@x), #0())] = [4]
> [0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [4]
>= [4]
= [#compare(@x, @y)]
[findMin#2(::(@y, @ys), @x)] = [1] @ys + [0]
? [1] @ys + [4]
= [findMin#3(#less(@x, @y), @x, @y, @ys)]
[findMin#2(nil(), @x)] = [0]
>= [0]
= [::(@x, nil())]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
, minSort#1(nil()) -> nil()
, 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()) }
Weak Trs:
{ findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
, findMin#1(nil()) -> nil()
, #cklt(#LT()) -> #true()
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, findMin(@l) -> findMin#1(@l)
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, minSort(@l) -> minSort#1(findMin(@l))
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
Uargs(#cklt) = {1}, Uargs(findMin#2) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[minSort#1](x1) = [1] x1 + [1]
[#true] = [0]
[#false] = [0]
[findMin#3](x1, x2, x3, x4) = [1] x1 + [1] x4 + [0]
[::](x1, x2) = [1] x2 + [0]
[#LT] = [0]
[findMin#1](x1) = [1]
[#cklt](x1) = [1] x1 + [0]
[#pos](x1) = [1] x1 + [0]
[#0] = [0]
[findMin](x1) = [1]
[#neg](x1) = [1] x1 + [0]
[#EQ] = [0]
[#less](x1, x2) = [4]
[minSort](x1) = [1] x1 + [4]
[#compare](x1, x2) = [4]
[#s](x1) = [1] x1 + [0]
[#GT] = [0]
[nil] = [0]
[findMin#2](x1, x2) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[minSort#1(::(@x, @xs))] = [1] @xs + [1]
? [1] @xs + [4]
= [::(@x, minSort(@xs))]
[minSort#1(nil())] = [1]
> [0]
= [nil()]
[findMin#3(#true(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@x, ::(@y, @ys))]
[findMin#3(#false(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@y, ::(@x, @ys))]
[findMin#1(::(@x, @xs))] = [1]
>= [1]
= [findMin#2(findMin(@xs), @x)]
[findMin#1(nil())] = [1]
> [0]
= [nil()]
[#cklt(#LT())] = [0]
>= [0]
= [#true()]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[findMin(@l)] = [1]
>= [1]
= [findMin#1(@l)]
[#less(@x, @y)] = [4]
>= [4]
= [#cklt(#compare(@x, @y))]
[minSort(@l)] = [1] @l + [4]
> [2]
= [minSort#1(findMin(@l))]
[#compare(#pos(@x), #pos(@y))] = [4]
>= [4]
= [#compare(@x, @y)]
[#compare(#pos(@x), #0())] = [4]
> [0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [4]
> [0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [4]
> [0]
= [#LT()]
[#compare(#0(), #0())] = [4]
> [0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [4]
> [0]
= [#GT()]
[#compare(#0(), #s(@y))] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #pos(@y))] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #0())] = [4]
> [0]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [4]
>= [4]
= [#compare(@y, @x)]
[#compare(#s(@x), #0())] = [4]
> [0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [4]
>= [4]
= [#compare(@x, @y)]
[findMin#2(::(@y, @ys), @x)] = [1] @ys + [0]
? [1] @ys + [4]
= [findMin#3(#less(@x, @y), @x, @y, @ys)]
[findMin#2(nil(), @x)] = [0]
>= [0]
= [::(@x, nil())]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
, 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()) }
Weak Trs:
{ minSort#1(nil()) -> nil()
, findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
, findMin#1(nil()) -> nil()
, #cklt(#LT()) -> #true()
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, findMin(@l) -> findMin#1(@l)
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, minSort(@l) -> minSort#1(findMin(@l))
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
Uargs(#cklt) = {1}, Uargs(findMin#2) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[minSort#1](x1) = [1] x1 + [0]
[#true] = [2]
[#false] = [2]
[findMin#3](x1, x2, x3, x4) = [1] x1 + [1] x4 + [4]
[::](x1, x2) = [1] x2 + [1]
[#LT] = [1]
[findMin#1](x1) = [1] x1 + [0]
[#cklt](x1) = [1] x1 + [2]
[#pos](x1) = [1] x1 + [0]
[#0] = [0]
[findMin](x1) = [1] x1 + [0]
[#neg](x1) = [1] x1 + [0]
[#EQ] = [0]
[#less](x1, x2) = [4]
[minSort](x1) = [1] x1 + [7]
[#compare](x1, x2) = [1]
[#s](x1) = [1] x1 + [0]
[#GT] = [0]
[nil] = [1]
[findMin#2](x1, x2) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[minSort#1(::(@x, @xs))] = [1] @xs + [1]
? [1] @xs + [8]
= [::(@x, minSort(@xs))]
[minSort#1(nil())] = [1]
>= [1]
= [nil()]
[findMin#3(#true(), @x, @y, @ys)] = [1] @ys + [6]
> [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[findMin#3(#false(), @x, @y, @ys)] = [1] @ys + [6]
> [1] @ys + [2]
= [::(@y, ::(@x, @ys))]
[findMin#1(::(@x, @xs))] = [1] @xs + [1]
> [1] @xs + [0]
= [findMin#2(findMin(@xs), @x)]
[findMin#1(nil())] = [1]
>= [1]
= [nil()]
[#cklt(#LT())] = [3]
> [2]
= [#true()]
[#cklt(#EQ())] = [2]
>= [2]
= [#false()]
[#cklt(#GT())] = [2]
>= [2]
= [#false()]
[findMin(@l)] = [1] @l + [0]
>= [1] @l + [0]
= [findMin#1(@l)]
[#less(@x, @y)] = [4]
> [3]
= [#cklt(#compare(@x, @y))]
[minSort(@l)] = [1] @l + [7]
> [1] @l + [0]
= [minSort#1(findMin(@l))]
[#compare(#pos(@x), #pos(@y))] = [1]
>= [1]
= [#compare(@x, @y)]
[#compare(#pos(@x), #0())] = [1]
> [0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [1]
> [0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [1]
>= [1]
= [#LT()]
[#compare(#0(), #0())] = [1]
> [0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [1]
> [0]
= [#GT()]
[#compare(#0(), #s(@y))] = [1]
>= [1]
= [#LT()]
[#compare(#neg(@x), #pos(@y))] = [1]
>= [1]
= [#LT()]
[#compare(#neg(@x), #0())] = [1]
>= [1]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [1]
>= [1]
= [#compare(@y, @x)]
[#compare(#s(@x), #0())] = [1]
> [0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [1]
>= [1]
= [#compare(@x, @y)]
[findMin#2(::(@y, @ys), @x)] = [1] @ys + [1]
? [1] @ys + [8]
= [findMin#3(#less(@x, @y), @x, @y, @ys)]
[findMin#2(nil(), @x)] = [1]
? [2]
= [::(@x, nil())]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
, findMin#2(::(@y, @ys), @x) ->
findMin#3(#less(@x, @y), @x, @y, @ys)
, findMin#2(nil(), @x) -> ::(@x, nil()) }
Weak Trs:
{ minSort#1(nil()) -> nil()
, findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
, findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
, findMin#1(nil()) -> nil()
, #cklt(#LT()) -> #true()
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, findMin(@l) -> findMin#1(@l)
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, minSort(@l) -> minSort#1(findMin(@l))
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs: { minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
Uargs(#cklt) = {1}, Uargs(findMin#2) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[minSort#1](x1) = [2] x1 + [0]
[#true] = [7]
[#false] = [7]
[findMin#3](x1, x2, x3, x4) = [1] x1 + [1] x4 + [7]
[::](x1, x2) = [1] x2 + [7]
[#LT] = [1]
[findMin#1](x1) = [1] x1 + [0]
[#cklt](x1) = [7] x1 + [0]
[#pos](x1) = [1] x1 + [0]
[#0] = [0]
[findMin](x1) = [1] x1 + [0]
[#neg](x1) = [1] x1 + [0]
[#EQ] = [1]
[#less](x1, x2) = [7]
[minSort](x1) = [2] x1 + [4]
[#compare](x1, x2) = [1]
[#s](x1) = [1] x1 + [0]
[#GT] = [1]
[nil] = [0]
[findMin#2](x1, x2) = [1] x1 + [7]
The order satisfies the following ordering constraints:
[minSort#1(::(@x, @xs))] = [2] @xs + [14]
> [2] @xs + [11]
= [::(@x, minSort(@xs))]
[minSort#1(nil())] = [0]
>= [0]
= [nil()]
[findMin#3(#true(), @x, @y, @ys)] = [1] @ys + [14]
>= [1] @ys + [14]
= [::(@x, ::(@y, @ys))]
[findMin#3(#false(), @x, @y, @ys)] = [1] @ys + [14]
>= [1] @ys + [14]
= [::(@y, ::(@x, @ys))]
[findMin#1(::(@x, @xs))] = [1] @xs + [7]
>= [1] @xs + [7]
= [findMin#2(findMin(@xs), @x)]
[findMin#1(nil())] = [0]
>= [0]
= [nil()]
[#cklt(#LT())] = [7]
>= [7]
= [#true()]
[#cklt(#EQ())] = [7]
>= [7]
= [#false()]
[#cklt(#GT())] = [7]
>= [7]
= [#false()]
[findMin(@l)] = [1] @l + [0]
>= [1] @l + [0]
= [findMin#1(@l)]
[#less(@x, @y)] = [7]
>= [7]
= [#cklt(#compare(@x, @y))]
[minSort(@l)] = [2] @l + [4]
> [2] @l + [0]
= [minSort#1(findMin(@l))]
[#compare(#pos(@x), #pos(@y))] = [1]
>= [1]
= [#compare(@x, @y)]
[#compare(#pos(@x), #0())] = [1]
>= [1]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [1]
>= [1]
= [#GT()]
[#compare(#0(), #pos(@y))] = [1]
>= [1]
= [#LT()]
[#compare(#0(), #0())] = [1]
>= [1]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [1]
>= [1]
= [#GT()]
[#compare(#0(), #s(@y))] = [1]
>= [1]
= [#LT()]
[#compare(#neg(@x), #pos(@y))] = [1]
>= [1]
= [#LT()]
[#compare(#neg(@x), #0())] = [1]
>= [1]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [1]
>= [1]
= [#compare(@y, @x)]
[#compare(#s(@x), #0())] = [1]
>= [1]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [1]
>= [1]
= [#compare(@x, @y)]
[findMin#2(::(@y, @ys), @x)] = [1] @ys + [14]
>= [1] @ys + [14]
= [findMin#3(#less(@x, @y), @x, @y, @ys)]
[findMin#2(nil(), @x)] = [7]
>= [7]
= [::(@x, nil())]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ findMin#2(::(@y, @ys), @x) ->
findMin#3(#less(@x, @y), @x, @y, @ys)
, findMin#2(nil(), @x) -> ::(@x, nil()) }
Weak Trs:
{ minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
, minSort#1(nil()) -> nil()
, findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
, findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
, findMin#1(nil()) -> nil()
, #cklt(#LT()) -> #true()
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, findMin(@l) -> findMin#1(@l)
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, minSort(@l) -> minSort#1(findMin(@l))
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
Trs: { findMin#2(nil(), @x) -> ::(@x, nil()) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
Uargs(#cklt) = {1}, Uargs(findMin#2) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA) and not(IDA(1)).
[minSort#1](x1) = [3 1] x1 + [3]
[0 1] [0]
[#true] = [2]
[0]
[#false] = [2]
[2]
[findMin#3](x1, x2, x3, x4) = [4 0] x1 + [0 2] x2 + [0 2] x3 + [1
4] x4 + [6]
[0 0] [0 0] [0 0] [0
0] [3]
[::](x1, x2) = [0 2] x1 + [1 4] x2 + [1]
[0 0] [0 0] [3]
[#LT] = [0]
[0]
[findMin#1](x1) = [1 2] x1 + [1]
[0 1] [0]
[#cklt](x1) = [2 0] x1 + [2]
[0 1] [0]
[#pos](x1) = [1 0] x1 + [0]
[0 1] [0]
[#0] = [0]
[5]
[findMin](x1) = [1 2] x1 + [1]
[0 1] [0]
[#neg](x1) = [1 1] x1 + [0]
[0 0] [4]
[#EQ] = [0]
[4]
[#less](x1, x2) = [0 0] x1 + [0 0] x2 + [2]
[4 0] [4 1] [0]
[minSort](x1) = [3 7] x1 + [7]
[0 1] [0]
[#compare](x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[4 0] [4 1] [0]
[#s](x1) = [1 0] x1 + [0]
[0 1] [0]
[#GT] = [0]
[4]
[nil] = [0]
[0]
[findMin#2](x1, x2) = [1 2] x1 + [0 2] x2 + [7]
[0 0] [0 0] [3]
The order satisfies the following ordering constraints:
[minSort#1(::(@x, @xs))] = [0 6] @x + [3 12] @xs + [9]
[0 0] [0 0] [3]
> [0 2] @x + [3 11] @xs + [8]
[0 0] [0 0] [3]
= [::(@x, minSort(@xs))]
[minSort#1(nil())] = [3]
[0]
> [0]
[0]
= [nil()]
[findMin#3(#true(), @x, @y, @ys)] = [0 2] @x + [0 2] @y + [1 4] @ys + [14]
[0 0] [0 0] [0 0] [3]
>= [0 2] @x + [0 2] @y + [1 4] @ys + [14]
[0 0] [0 0] [0 0] [3]
= [::(@x, ::(@y, @ys))]
[findMin#3(#false(), @x, @y, @ys)] = [0 2] @x + [0 2] @y + [1 4] @ys + [14]
[0 0] [0 0] [0 0] [3]
>= [0 2] @x + [0 2] @y + [1 4] @ys + [14]
[0 0] [0 0] [0 0] [3]
= [::(@y, ::(@x, @ys))]
[findMin#1(::(@x, @xs))] = [0 2] @x + [1 4] @xs + [8]
[0 0] [0 0] [3]
>= [0 2] @x + [1 4] @xs + [8]
[0 0] [0 0] [3]
= [findMin#2(findMin(@xs), @x)]
[findMin#1(nil())] = [1]
[0]
> [0]
[0]
= [nil()]
[#cklt(#LT())] = [2]
[0]
>= [2]
[0]
= [#true()]
[#cklt(#EQ())] = [2]
[4]
>= [2]
[2]
= [#false()]
[#cklt(#GT())] = [2]
[4]
>= [2]
[2]
= [#false()]
[findMin(@l)] = [1 2] @l + [1]
[0 1] [0]
>= [1 2] @l + [1]
[0 1] [0]
= [findMin#1(@l)]
[#less(@x, @y)] = [0 0] @x + [0 0] @y + [2]
[4 0] [4 1] [0]
>= [0 0] @x + [0 0] @y + [2]
[4 0] [4 1] [0]
= [#cklt(#compare(@x, @y))]
[minSort(@l)] = [3 7] @l + [7]
[0 1] [0]
> [3 7] @l + [6]
[0 1] [0]
= [minSort#1(findMin(@l))]
[#compare(#pos(@x), #pos(@y))] = [0 0] @x + [0 0] @y + [0]
[4 0] [4 1] [0]
>= [0 0] @x + [0 0] @y + [0]
[4 0] [4 1] [0]
= [#compare(@x, @y)]
[#compare(#pos(@x), #0())] = [0 0] @x + [0]
[4 0] [5]
>= [0]
[4]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [0 0] @x + [0 0] @y + [0]
[4 0] [4 4] [4]
>= [0]
[4]
= [#GT()]
[#compare(#0(), #pos(@y))] = [0 0] @y + [0]
[4 1] [0]
>= [0]
[0]
= [#LT()]
[#compare(#0(), #0())] = [0]
[5]
>= [0]
[4]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [0 0] @y + [0]
[4 4] [4]
>= [0]
[4]
= [#GT()]
[#compare(#0(), #s(@y))] = [0 0] @y + [0]
[4 1] [0]
>= [0]
[0]
= [#LT()]
[#compare(#neg(@x), #pos(@y))] = [0 0] @x + [0 0] @y + [0]
[4 4] [4 1] [0]
>= [0]
[0]
= [#LT()]
[#compare(#neg(@x), #0())] = [0 0] @x + [0]
[4 4] [5]
>= [0]
[0]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [0 0] @x + [0 0] @y + [0]
[4 4] [4 4] [4]
>= [0 0] @x + [0 0] @y + [0]
[4 1] [4 0] [0]
= [#compare(@y, @x)]
[#compare(#s(@x), #0())] = [0 0] @x + [0]
[4 0] [5]
>= [0]
[4]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [0 0] @x + [0 0] @y + [0]
[4 0] [4 1] [0]
>= [0 0] @x + [0 0] @y + [0]
[4 0] [4 1] [0]
= [#compare(@x, @y)]
[findMin#2(::(@y, @ys), @x)] = [0 2] @x + [0 2] @y + [1 4] @ys + [14]
[0 0] [0 0] [0 0] [3]
>= [0 2] @x + [0 2] @y + [1 4] @ys + [14]
[0 0] [0 0] [0 0] [3]
= [findMin#3(#less(@x, @y), @x, @y, @ys)]
[findMin#2(nil(), @x)] = [0 2] @x + [7]
[0 0] [3]
> [0 2] @x + [1]
[0 0] [3]
= [::(@x, nil())]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ findMin#2(::(@y, @ys), @x) ->
findMin#3(#less(@x, @y), @x, @y, @ys) }
Weak Trs:
{ minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
, minSort#1(nil()) -> nil()
, findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
, findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
, findMin#1(nil()) -> nil()
, #cklt(#LT()) -> #true()
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, findMin(@l) -> findMin#1(@l)
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, minSort(@l) -> minSort#1(findMin(@l))
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, findMin#2(nil(), @x) -> ::(@x, nil()) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
Trs:
{ findMin#2(::(@y, @ys), @x) ->
findMin#3(#less(@x, @y), @x, @y, @ys) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
Uargs(#cklt) = {1}, Uargs(findMin#2) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[minSort#1](x1) = [4 0] x1 + [1]
[0 2] [0]
[#true] = [3]
[0]
[#false] = [3]
[0]
[findMin#3](x1, x2, x3, x4) = [1 1] x1 + [0 2] x2 + [0 2] x3 + [1
4] x4 + [7]
[0 0] [0 0] [0 0] [0
1] [4]
[::](x1, x2) = [0 2] x1 + [1 2] x2 + [3]
[0 0] [0 1] [2]
[#LT] = [1]
[1]
[findMin#1](x1) = [1 1] x1 + [1]
[0 1] [0]
[#cklt](x1) = [1 1] x1 + [1]
[0 0] [0]
[#pos](x1) = [1 0] x1 + [0]
[0 1] [0]
[#0] = [0]
[0]
[findMin](x1) = [1 1] x1 + [1]
[0 1] [0]
[#neg](x1) = [1 0] x1 + [0]
[0 1] [0]
[#EQ] = [1]
[1]
[#less](x1, x2) = [3]
[0]
[minSort](x1) = [4 4] x1 + [6]
[0 2] [0]
[#compare](x1, x2) = [1]
[1]
[#s](x1) = [1 0] x1 + [2]
[0 1] [0]
[#GT] = [1]
[1]
[nil] = [1]
[0]
[findMin#2](x1, x2) = [1 2] x1 + [0 2] x2 + [5]
[0 1] [0 0] [2]
The order satisfies the following ordering constraints:
[minSort#1(::(@x, @xs))] = [0 8] @x + [4 8] @xs + [13]
[0 0] [0 2] [4]
> [0 2] @x + [4 8] @xs + [9]
[0 0] [0 2] [2]
= [::(@x, minSort(@xs))]
[minSort#1(nil())] = [5]
[0]
> [1]
[0]
= [nil()]
[findMin#3(#true(), @x, @y, @ys)] = [0 2] @x + [0 2] @y + [1 4] @ys + [10]
[0 0] [0 0] [0 1] [4]
>= [0 2] @x + [0 2] @y + [1 4] @ys + [10]
[0 0] [0 0] [0 1] [4]
= [::(@x, ::(@y, @ys))]
[findMin#3(#false(), @x, @y, @ys)] = [0 2] @x + [0 2] @y + [1 4] @ys + [10]
[0 0] [0 0] [0 1] [4]
>= [0 2] @x + [0 2] @y + [1 4] @ys + [10]
[0 0] [0 0] [0 1] [4]
= [::(@y, ::(@x, @ys))]
[findMin#1(::(@x, @xs))] = [0 2] @x + [1 3] @xs + [6]
[0 0] [0 1] [2]
>= [0 2] @x + [1 3] @xs + [6]
[0 0] [0 1] [2]
= [findMin#2(findMin(@xs), @x)]
[findMin#1(nil())] = [2]
[0]
> [1]
[0]
= [nil()]
[#cklt(#LT())] = [3]
[0]
>= [3]
[0]
= [#true()]
[#cklt(#EQ())] = [3]
[0]
>= [3]
[0]
= [#false()]
[#cklt(#GT())] = [3]
[0]
>= [3]
[0]
= [#false()]
[findMin(@l)] = [1 1] @l + [1]
[0 1] [0]
>= [1 1] @l + [1]
[0 1] [0]
= [findMin#1(@l)]
[#less(@x, @y)] = [3]
[0]
>= [3]
[0]
= [#cklt(#compare(@x, @y))]
[minSort(@l)] = [4 4] @l + [6]
[0 2] [0]
> [4 4] @l + [5]
[0 2] [0]
= [minSort#1(findMin(@l))]
[#compare(#pos(@x), #pos(@y))] = [1]
[1]
>= [1]
[1]
= [#compare(@x, @y)]
[#compare(#pos(@x), #0())] = [1]
[1]
>= [1]
[1]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [1]
[1]
>= [1]
[1]
= [#GT()]
[#compare(#0(), #pos(@y))] = [1]
[1]
>= [1]
[1]
= [#LT()]
[#compare(#0(), #0())] = [1]
[1]
>= [1]
[1]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [1]
[1]
>= [1]
[1]
= [#GT()]
[#compare(#0(), #s(@y))] = [1]
[1]
>= [1]
[1]
= [#LT()]
[#compare(#neg(@x), #pos(@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(#s(@x), #0())] = [1]
[1]
>= [1]
[1]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [1]
[1]
>= [1]
[1]
= [#compare(@x, @y)]
[findMin#2(::(@y, @ys), @x)] = [0 2] @x + [0 2] @y + [1 4] @ys + [12]
[0 0] [0 0] [0 1] [4]
> [0 2] @x + [0 2] @y + [1 4] @ys + [10]
[0 0] [0 0] [0 1] [4]
= [findMin#3(#less(@x, @y), @x, @y, @ys)]
[findMin#2(nil(), @x)] = [0 2] @x + [6]
[0 0] [2]
> [0 2] @x + [4]
[0 0] [2]
= [::(@x, nil())]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
, minSort#1(nil()) -> nil()
, findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
, findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
, findMin#1(nil()) -> nil()
, #cklt(#LT()) -> #true()
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, findMin(@l) -> findMin#1(@l)
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, minSort(@l) -> minSort#1(findMin(@l))
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, findMin#2(::(@y, @ys), @x) ->
findMin#3(#less(@x, @y), @x, @y, @ys)
, findMin#2(nil(), @x) -> ::(@x, nil()) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^2))