YES(O(1),O(n^3))
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Weak Trs:
{ #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs: { insertionsortD#1(nil()) -> 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(#cklt) = {1}, Uargs(insert) = {2}, Uargs(::) = {2},
Uargs(insert#2) = {1}, Uargs(insertD) = {2}, Uargs(insertD#2) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#0] = [0]
[#abs](x1) = [0]
[#neg](x1) = [1] x1 + [0]
[#pos](x1) = [0]
[#s](x1) = [1] x1 + [0]
[#less](x1, x2) = [0]
[#compare](x1, x2) = [0]
[#cklt](x1) = [1] x1 + [0]
[insert](x1, x2) = [2] x2 + [0]
[insert#1](x1, x2) = [2] x1 + [0]
[::](x1, x2) = [1] x2 + [0]
[insert#2](x1, x2, x3, x4) = [2] x1 + [2] x4 + [0]
[nil] = [0]
[#false] = [0]
[#true] = [0]
[insertD](x1, x2) = [1] x2 + [0]
[insertD#1](x1, x2) = [1] x1 + [0]
[insertD#2](x1, x2, x3, x4) = [1] x1 + [1] x4 + [0]
[insertionsort](x1) = [0]
[insertionsort#1](x1) = [0]
[insertionsortD](x1) = [1]
[insertionsortD#1](x1) = [1]
[#EQ] = [0]
[#GT] = [0]
[#LT] = [0]
This order satisfies following ordering constraints
[#abs(#0())] = [0]
>= [0]
= [#0()]
[#abs(#neg(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#pos(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#s(@x))] = [0]
>= [0]
= [#pos(#s(@x))]
[#less(@x, @y)] = [0]
>= [0]
= [#cklt(#compare(@x, @y))]
[#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)]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[#cklt(#LT())] = [0]
>= [0]
= [#true()]
[insert(@x, @l)] = [2] @l + [0]
>= [2] @l + [0]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [2] @ys + [0]
>= [2] @ys + [0]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [0]
>= [0]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [2] @ys + [0]
>= [1] @ys + [0]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [2] @ys + [0]
>= [2] @ys + [0]
= [::(@y, insert(@x, @ys))]
[insertD(@x, @l)] = [1] @l + [0]
>= [1] @l + [0]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [1] @ys + [0]
>= [1] @ys + [0]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [0]
>= [0]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@y, insertD(@x, @ys))]
[insertionsort(@l)] = [0]
>= [0]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [0]
>= [0]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [0]
>= [0]
= [nil()]
[insertionsortD(@l)] = [1]
>= [1]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [1]
>= [1]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [1]
> [0]
= [nil()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) ->
insertD(@x, insertionsortD(@xs)) }
Weak Trs:
{ #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs: { insertionsort#1(nil()) -> 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(#cklt) = {1}, Uargs(insert) = {2}, Uargs(::) = {2},
Uargs(insert#2) = {1}, Uargs(insertD) = {2}, Uargs(insertD#2) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#0] = [0]
[#abs](x1) = [0]
[#neg](x1) = [1] x1 + [0]
[#pos](x1) = [0]
[#s](x1) = [1] x1 + [0]
[#less](x1, x2) = [0]
[#compare](x1, x2) = [0]
[#cklt](x1) = [2] x1 + [0]
[insert](x1, x2) = [1] x2 + [0]
[insert#1](x1, x2) = [1] x1 + [0]
[::](x1, x2) = [1] x2 + [0]
[insert#2](x1, x2, x3, x4) = [1] x1 + [1] x4 + [0]
[nil] = [0]
[#false] = [0]
[#true] = [0]
[insertD](x1, x2) = [1] x2 + [0]
[insertD#1](x1, x2) = [1] x1 + [0]
[insertD#2](x1, x2, x3, x4) = [1] x1 + [1] x4 + [0]
[insertionsort](x1) = [1]
[insertionsort#1](x1) = [1]
[insertionsortD](x1) = [1] x1 + [1]
[insertionsortD#1](x1) = [1] x1 + [1]
[#EQ] = [0]
[#GT] = [0]
[#LT] = [0]
This order satisfies following ordering constraints
[#abs(#0())] = [0]
>= [0]
= [#0()]
[#abs(#neg(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#pos(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#s(@x))] = [0]
>= [0]
= [#pos(#s(@x))]
[#less(@x, @y)] = [0]
>= [0]
= [#cklt(#compare(@x, @y))]
[#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)]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[#cklt(#LT())] = [0]
>= [0]
= [#true()]
[insert(@x, @l)] = [1] @l + [0]
>= [1] @l + [0]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [1] @ys + [0]
>= [1] @ys + [0]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [0]
>= [0]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@y, insert(@x, @ys))]
[insertD(@x, @l)] = [1] @l + [0]
>= [1] @l + [0]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [1] @ys + [0]
>= [1] @ys + [0]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [0]
>= [0]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [1] @ys + [0]
>= [1] @ys + [0]
= [::(@y, insertD(@x, @ys))]
[insertionsort(@l)] = [1]
>= [1]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [1]
>= [1]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [1]
> [0]
= [nil()]
[insertionsortD(@l)] = [1] @l + [1]
>= [1] @l + [1]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [1] @xs + [1]
>= [1] @xs + [1]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [1]
> [0]
= [nil()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) ->
insertD(@x, insertionsortD(@xs)) }
Weak Trs:
{ #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, insertionsort#1(nil()) -> nil()
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs:
{ insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@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(#cklt) = {1}, Uargs(insert) = {2}, Uargs(::) = {2},
Uargs(insert#2) = {1}, Uargs(insertD) = {2}, Uargs(insertD#2) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#0] = [0]
[#abs](x1) = [0]
[#neg](x1) = [1] x1 + [0]
[#pos](x1) = [0]
[#s](x1) = [1] x1 + [0]
[#less](x1, x2) = [0]
[#compare](x1, x2) = [0]
[#cklt](x1) = [2] x1 + [0]
[insert](x1, x2) = [1] x2 + [1]
[insert#1](x1, x2) = [1] x1 + [1]
[::](x1, x2) = [1] x2 + [1]
[insert#2](x1, x2, x3, x4) = [2] x1 + [1] x4 + [2]
[nil] = [1]
[#false] = [0]
[#true] = [0]
[insertD](x1, x2) = [1] x2 + [1]
[insertD#1](x1, x2) = [1] x1 + [1]
[insertD#2](x1, x2, x3, x4) = [1] x1 + [1] x4 + [2]
[insertionsort](x1) = [2] x1 + [0]
[insertionsort#1](x1) = [2] x1 + [0]
[insertionsortD](x1) = [1] x1 + [0]
[insertionsortD#1](x1) = [1] x1 + [0]
[#EQ] = [0]
[#GT] = [0]
[#LT] = [0]
This order satisfies following ordering constraints
[#abs(#0())] = [0]
>= [0]
= [#0()]
[#abs(#neg(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#pos(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#s(@x))] = [0]
>= [0]
= [#pos(#s(@x))]
[#less(@x, @y)] = [0]
>= [0]
= [#cklt(#compare(@x, @y))]
[#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)]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[#cklt(#LT())] = [0]
>= [0]
= [#true()]
[insert(@x, @l)] = [1] @l + [1]
>= [1] @l + [1]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [1] @ys + [2]
>= [1] @ys + [2]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [2]
>= [2]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@y, insert(@x, @ys))]
[insertD(@x, @l)] = [1] @l + [1]
>= [1] @l + [1]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [1] @ys + [2]
>= [1] @ys + [2]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [2]
>= [2]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@y, insertD(@x, @ys))]
[insertionsort(@l)] = [2] @l + [0]
>= [2] @l + [0]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [2] @xs + [2]
> [2] @xs + [1]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [2]
> [1]
= [nil()]
[insertionsortD(@l)] = [1] @l + [0]
>= [1] @l + [0]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [1] @xs + [1]
>= [1] @xs + [1]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [1]
>= [1]
= [nil()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) ->
insertD(@x, insertionsortD(@xs)) }
Weak Trs:
{ #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs:
{ insertionsortD#1(::(@x, @xs)) ->
insertD(@x, insertionsortD(@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(#cklt) = {1}, Uargs(insert) = {2}, Uargs(::) = {2},
Uargs(insert#2) = {1}, Uargs(insertD) = {2}, Uargs(insertD#2) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#0] = [0]
[#abs](x1) = [0]
[#neg](x1) = [1] x1 + [0]
[#pos](x1) = [0]
[#s](x1) = [1] x1 + [0]
[#less](x1, x2) = [0]
[#compare](x1, x2) = [0]
[#cklt](x1) = [2] x1 + [0]
[insert](x1, x2) = [1] x2 + [1]
[insert#1](x1, x2) = [1] x1 + [1]
[::](x1, x2) = [1] x2 + [1]
[insert#2](x1, x2, x3, x4) = [2] x1 + [1] x4 + [2]
[nil] = [2]
[#false] = [0]
[#true] = [0]
[insertD](x1, x2) = [1] x2 + [1]
[insertD#1](x1, x2) = [1] x1 + [1]
[insertD#2](x1, x2, x3, x4) = [1] x1 + [1] x4 + [2]
[insertionsort](x1) = [1] x1 + [0]
[insertionsort#1](x1) = [1] x1 + [0]
[insertionsortD](x1) = [2] x1 + [1]
[insertionsortD#1](x1) = [2] x1 + [1]
[#EQ] = [0]
[#GT] = [0]
[#LT] = [0]
This order satisfies following ordering constraints
[#abs(#0())] = [0]
>= [0]
= [#0()]
[#abs(#neg(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#pos(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#s(@x))] = [0]
>= [0]
= [#pos(#s(@x))]
[#less(@x, @y)] = [0]
>= [0]
= [#cklt(#compare(@x, @y))]
[#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)]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[#cklt(#LT())] = [0]
>= [0]
= [#true()]
[insert(@x, @l)] = [1] @l + [1]
>= [1] @l + [1]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [1] @ys + [2]
>= [1] @ys + [2]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [3]
>= [3]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@y, insert(@x, @ys))]
[insertD(@x, @l)] = [1] @l + [1]
>= [1] @l + [1]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [1] @ys + [2]
>= [1] @ys + [2]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [3]
>= [3]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@y, insertD(@x, @ys))]
[insertionsort(@l)] = [1] @l + [0]
>= [1] @l + [0]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [1] @xs + [1]
>= [1] @xs + [1]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [2]
>= [2]
= [nil()]
[insertionsortD(@l)] = [2] @l + [1]
>= [2] @l + [1]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [2] @xs + [3]
> [2] @xs + [2]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [5]
> [2]
= [nil()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsortD(@l) -> insertionsortD#1(@l) }
Weak Trs:
{ #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs: { insertionsort(@l) -> insertionsort#1(@l) }
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(#cklt) = {1}, Uargs(insert) = {2}, Uargs(::) = {2},
Uargs(insert#2) = {1}, Uargs(insertD) = {2}, Uargs(insertD#2) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#0] = [0]
[#abs](x1) = [0]
[#neg](x1) = [1] x1 + [0]
[#pos](x1) = [0]
[#s](x1) = [1] x1 + [0]
[#less](x1, x2) = [0]
[#compare](x1, x2) = [0]
[#cklt](x1) = [2] x1 + [0]
[insert](x1, x2) = [1] x2 + [1]
[insert#1](x1, x2) = [1] x1 + [1]
[::](x1, x2) = [1] x2 + [1]
[insert#2](x1, x2, x3, x4) = [1] x1 + [1] x4 + [2]
[nil] = [0]
[#false] = [0]
[#true] = [0]
[insertD](x1, x2) = [1] x2 + [1]
[insertD#1](x1, x2) = [1] x1 + [1]
[insertD#2](x1, x2, x3, x4) = [1] x1 + [1] x4 + [2]
[insertionsort](x1) = [2] x1 + [2]
[insertionsort#1](x1) = [2] x1 + [1]
[insertionsortD](x1) = [1] x1 + [0]
[insertionsortD#1](x1) = [1] x1 + [0]
[#EQ] = [0]
[#GT] = [0]
[#LT] = [0]
This order satisfies following ordering constraints
[#abs(#0())] = [0]
>= [0]
= [#0()]
[#abs(#neg(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#pos(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#s(@x))] = [0]
>= [0]
= [#pos(#s(@x))]
[#less(@x, @y)] = [0]
>= [0]
= [#cklt(#compare(@x, @y))]
[#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)]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[#cklt(#LT())] = [0]
>= [0]
= [#true()]
[insert(@x, @l)] = [1] @l + [1]
>= [1] @l + [1]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [1] @ys + [2]
>= [1] @ys + [2]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [1]
>= [1]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@y, insert(@x, @ys))]
[insertD(@x, @l)] = [1] @l + [1]
>= [1] @l + [1]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [1] @ys + [2]
>= [1] @ys + [2]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [1]
>= [1]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@y, insertD(@x, @ys))]
[insertionsort(@l)] = [2] @l + [2]
> [2] @l + [1]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [2] @xs + [3]
>= [2] @xs + [3]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [1]
> [0]
= [nil()]
[insertionsortD(@l)] = [1] @l + [0]
>= [1] @l + [0]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [1] @xs + [1]
>= [1] @xs + [1]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [0]
>= [0]
= [nil()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsortD(@l) -> insertionsortD#1(@l) }
Weak Trs:
{ #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs: { insertionsortD(@l) -> insertionsortD#1(@l) }
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(#cklt) = {1}, Uargs(insert) = {2}, Uargs(::) = {2},
Uargs(insert#2) = {1}, Uargs(insertD) = {2}, Uargs(insertD#2) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#0] = [0]
[#abs](x1) = [0]
[#neg](x1) = [1] x1 + [0]
[#pos](x1) = [0]
[#s](x1) = [1] x1 + [0]
[#less](x1, x2) = [0]
[#compare](x1, x2) = [0]
[#cklt](x1) = [2] x1 + [0]
[insert](x1, x2) = [1] x2 + [1]
[insert#1](x1, x2) = [1] x1 + [1]
[::](x1, x2) = [1] x2 + [1]
[insert#2](x1, x2, x3, x4) = [2] x1 + [1] x4 + [2]
[nil] = [0]
[#false] = [0]
[#true] = [0]
[insertD](x1, x2) = [1] x2 + [1]
[insertD#1](x1, x2) = [1] x1 + [1]
[insertD#2](x1, x2, x3, x4) = [1] x1 + [1] x4 + [2]
[insertionsort](x1) = [1] x1 + [0]
[insertionsort#1](x1) = [1] x1 + [0]
[insertionsortD](x1) = [2] x1 + [1]
[insertionsortD#1](x1) = [2] x1 + [0]
[#EQ] = [0]
[#GT] = [0]
[#LT] = [0]
This order satisfies following ordering constraints
[#abs(#0())] = [0]
>= [0]
= [#0()]
[#abs(#neg(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#pos(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#s(@x))] = [0]
>= [0]
= [#pos(#s(@x))]
[#less(@x, @y)] = [0]
>= [0]
= [#cklt(#compare(@x, @y))]
[#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)]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[#cklt(#LT())] = [0]
>= [0]
= [#true()]
[insert(@x, @l)] = [1] @l + [1]
>= [1] @l + [1]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [1] @ys + [2]
>= [1] @ys + [2]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [1]
>= [1]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@y, insert(@x, @ys))]
[insertD(@x, @l)] = [1] @l + [1]
>= [1] @l + [1]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [1] @ys + [2]
>= [1] @ys + [2]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [1]
>= [1]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@y, insertD(@x, @ys))]
[insertionsort(@l)] = [1] @l + [0]
>= [1] @l + [0]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [1] @xs + [1]
>= [1] @xs + [1]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [0]
>= [0]
= [nil()]
[insertionsortD(@l)] = [2] @l + [1]
> [2] @l + [0]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [2] @xs + [2]
>= [2] @xs + [2]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [0]
>= [0]
= [nil()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys)) }
Weak Trs:
{ #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs:
{ insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) }
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(#cklt) = {1}, Uargs(insert) = {2}, Uargs(::) = {2},
Uargs(insert#2) = {1}, Uargs(insertD) = {2}, Uargs(insertD#2) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#0] = [0]
[#abs](x1) = [0]
[#neg](x1) = [1] x1 + [0]
[#pos](x1) = [0]
[#s](x1) = [1] x1 + [0]
[#less](x1, x2) = [1]
[#compare](x1, x2) = [0]
[#cklt](x1) = [2] x1 + [1]
[insert](x1, x2) = [1] x2 + [1]
[insert#1](x1, x2) = [1] x1 + [1]
[::](x1, x2) = [1] x2 + [1]
[insert#2](x1, x2, x3, x4) = [2] x1 + [1] x4 + [0]
[nil] = [1]
[#false] = [1]
[#true] = [1]
[insertD](x1, x2) = [1] x2 + [2]
[insertD#1](x1, x2) = [1] x1 + [2]
[insertD#2](x1, x2, x3, x4) = [2] x1 + [1] x4 + [1]
[insertionsort](x1) = [1] x1 + [0]
[insertionsort#1](x1) = [1] x1 + [0]
[insertionsortD](x1) = [2] x1 + [1]
[insertionsortD#1](x1) = [2] x1 + [1]
[#EQ] = [0]
[#GT] = [0]
[#LT] = [0]
This order satisfies following ordering constraints
[#abs(#0())] = [0]
>= [0]
= [#0()]
[#abs(#neg(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#pos(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#s(@x))] = [0]
>= [0]
= [#pos(#s(@x))]
[#less(@x, @y)] = [1]
>= [1]
= [#cklt(#compare(@x, @y))]
[#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)]
[#cklt(#EQ())] = [1]
>= [1]
= [#false()]
[#cklt(#GT())] = [1]
>= [1]
= [#false()]
[#cklt(#LT())] = [1]
>= [1]
= [#true()]
[insert(@x, @l)] = [1] @l + [1]
>= [1] @l + [1]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [1] @ys + [2]
>= [1] @ys + [2]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [2]
>= [2]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@y, insert(@x, @ys))]
[insertD(@x, @l)] = [1] @l + [2]
>= [1] @l + [2]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [1] @ys + [3]
>= [1] @ys + [3]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [3]
> [2]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [1] @ys + [3]
> [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [1] @ys + [3]
>= [1] @ys + [3]
= [::(@y, insertD(@x, @ys))]
[insertionsort(@l)] = [1] @l + [0]
>= [1] @l + [0]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [1] @xs + [1]
>= [1] @xs + [1]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [1]
>= [1]
= [nil()]
[insertionsortD(@l)] = [2] @l + [1]
>= [2] @l + [1]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [2] @xs + [3]
>= [2] @xs + [3]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [3]
> [1]
= [nil()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys)) }
Weak Trs:
{ #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs:
{ insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) }
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(#cklt) = {1}, Uargs(insert) = {2}, Uargs(::) = {2},
Uargs(insert#2) = {1}, Uargs(insertD) = {2}, Uargs(insertD#2) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#0] = [0]
[#abs](x1) = [0]
[#neg](x1) = [1] x1 + [0]
[#pos](x1) = [0]
[#s](x1) = [1] x1 + [0]
[#less](x1, x2) = [1]
[#compare](x1, x2) = [0]
[#cklt](x1) = [1] x1 + [1]
[insert](x1, x2) = [1] x2 + [2]
[insert#1](x1, x2) = [1] x1 + [2]
[::](x1, x2) = [1] x2 + [1]
[insert#2](x1, x2, x3, x4) = [2] x1 + [1] x4 + [1]
[nil] = [0]
[#false] = [1]
[#true] = [1]
[insertD](x1, x2) = [1] x2 + [1]
[insertD#1](x1, x2) = [1] x1 + [1]
[insertD#2](x1, x2, x3, x4) = [1] x1 + [1] x4 + [1]
[insertionsort](x1) = [2] x1 + [1]
[insertionsort#1](x1) = [2] x1 + [1]
[insertionsortD](x1) = [2] x1 + [0]
[insertionsortD#1](x1) = [2] x1 + [0]
[#EQ] = [0]
[#GT] = [0]
[#LT] = [0]
This order satisfies following ordering constraints
[#abs(#0())] = [0]
>= [0]
= [#0()]
[#abs(#neg(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#pos(@x))] = [0]
>= [0]
= [#pos(@x)]
[#abs(#s(@x))] = [0]
>= [0]
= [#pos(#s(@x))]
[#less(@x, @y)] = [1]
>= [1]
= [#cklt(#compare(@x, @y))]
[#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)]
[#cklt(#EQ())] = [1]
>= [1]
= [#false()]
[#cklt(#GT())] = [1]
>= [1]
= [#false()]
[#cklt(#LT())] = [1]
>= [1]
= [#true()]
[insert(@x, @l)] = [1] @l + [2]
>= [1] @l + [2]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [1] @ys + [3]
>= [1] @ys + [3]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [2]
> [1]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [1] @ys + [3]
> [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [1] @ys + [3]
>= [1] @ys + [3]
= [::(@y, insert(@x, @ys))]
[insertD(@x, @l)] = [1] @l + [1]
>= [1] @l + [1]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [1] @ys + [2]
>= [1] @ys + [2]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [1]
>= [1]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@y, insertD(@x, @ys))]
[insertionsort(@l)] = [2] @l + [1]
>= [2] @l + [1]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [2] @xs + [3]
>= [2] @xs + [3]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [1]
> [0]
= [nil()]
[insertionsortD(@l)] = [2] @l + [0]
>= [2] @l + [0]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [2] @xs + [2]
> [2] @xs + [1]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [0]
>= [0]
= [nil()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys)) }
Weak Trs:
{ #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x)) }
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(#cklt) = {1}, Uargs(insert) = {2}, Uargs(::) = {2},
Uargs(insert#2) = {1}, Uargs(insertD) = {2}, Uargs(insertD#2) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#0] = [0]
[#abs](x1) = [1]
[#neg](x1) = [1] x1 + [0]
[#pos](x1) = [0]
[#s](x1) = [1] x1 + [0]
[#less](x1, x2) = [2]
[#compare](x1, x2) = [1]
[#cklt](x1) = [1] x1 + [1]
[insert](x1, x2) = [1] x2 + [2]
[insert#1](x1, x2) = [1] x1 + [2]
[::](x1, x2) = [1] x2 + [1]
[insert#2](x1, x2, x3, x4) = [1] x1 + [1] x4 + [1]
[nil] = [1]
[#false] = [1]
[#true] = [2]
[insertD](x1, x2) = [1] x2 + [2]
[insertD#1](x1, x2) = [1] x1 + [2]
[insertD#2](x1, x2, x3, x4) = [1] x1 + [1] x4 + [1]
[insertionsort](x1) = [2] x1 + [1]
[insertionsort#1](x1) = [2] x1 + [1]
[insertionsortD](x1) = [2] x1 + [0]
[insertionsortD#1](x1) = [2] x1 + [0]
[#EQ] = [0]
[#GT] = [0]
[#LT] = [1]
This order satisfies following ordering constraints
[#abs(#0())] = [1]
> [0]
= [#0()]
[#abs(#neg(@x))] = [1]
> [0]
= [#pos(@x)]
[#abs(#pos(@x))] = [1]
> [0]
= [#pos(@x)]
[#abs(#s(@x))] = [1]
> [0]
= [#pos(#s(@x))]
[#less(@x, @y)] = [2]
>= [2]
= [#cklt(#compare(@x, @y))]
[#compare(#0(), #0())] = [1]
> [0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [1]
> [0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [1]
>= [1]
= [#LT()]
[#compare(#0(), #s(@y))] = [1]
>= [1]
= [#LT()]
[#compare(#neg(@x), #0())] = [1]
>= [1]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [1]
>= [1]
= [#compare(@y, @x)]
[#compare(#neg(@x), #pos(@y))] = [1]
>= [1]
= [#LT()]
[#compare(#pos(@x), #0())] = [1]
> [0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [1]
> [0]
= [#GT()]
[#compare(#pos(@x), #pos(@y))] = [1]
>= [1]
= [#compare(@x, @y)]
[#compare(#s(@x), #0())] = [1]
> [0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [1]
>= [1]
= [#compare(@x, @y)]
[#cklt(#EQ())] = [1]
>= [1]
= [#false()]
[#cklt(#GT())] = [1]
>= [1]
= [#false()]
[#cklt(#LT())] = [2]
>= [2]
= [#true()]
[insert(@x, @l)] = [1] @l + [2]
>= [1] @l + [2]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [1] @ys + [3]
>= [1] @ys + [3]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [3]
> [2]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [1] @ys + [3]
>= [1] @ys + [3]
= [::(@y, insert(@x, @ys))]
[insertD(@x, @l)] = [1] @l + [2]
>= [1] @l + [2]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [1] @ys + [3]
>= [1] @ys + [3]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [3]
> [2]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [1] @ys + [2]
>= [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [1] @ys + [3]
>= [1] @ys + [3]
= [::(@y, insertD(@x, @ys))]
[insertionsort(@l)] = [2] @l + [1]
>= [2] @l + [1]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [2] @xs + [3]
>= [2] @xs + [3]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [3]
> [1]
= [nil()]
[insertionsortD(@l)] = [2] @l + [0]
>= [2] @l + [0]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [2] @xs + [2]
>= [2] @xs + [2]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [2]
> [1]
= [nil()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys)) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 4' to
orient following rules strictly.
Trs: { insert(@x, @l) -> insert#1(@l, @x) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^3)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(#cklt) = {1}, Uargs(insert) = {2}, Uargs(::) = {2},
Uargs(insert#2) = {1}, Uargs(insertD) = {2}, Uargs(insertD#2) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA) and not(IDA(3)).
[1]
[#0] = [0]
[1]
[1]
[1 1 1 1] [0]
[#abs](x1) = [1 1 0 1] x1 + [0]
[1 0 0 1] [0]
[1 0 0 1] [0]
[1 0 1 0] [0]
[#neg](x1) = [0 1 0 0] x1 + [0]
[0 1 0 0] [1]
[0 0 0 0] [1]
[0 1 0 0] [0]
[#pos](x1) = [0 0 0 0] x1 + [0]
[0 0 1 0] [1]
[0 0 1 0] [1]
[0 1 1 0] [0]
[#s](x1) = [0 1 0 0] x1 + [0]
[0 0 0 0] [0]
[0 1 0 1] [1]
[1]
[#less](x1, x2) = [0]
[0]
[1]
[0]
[#compare](x1, x2) = [0]
[0]
[0]
[1 0 0 0] [1]
[#cklt](x1) = [1 0 1 1] x1 + [0]
[0 0 0 0] [0]
[0 0 0 0] [1]
[1 0 1 0] [1 1 0 0] [1]
[insert](x1, x2) = [0 0 0 0] x1 + [0 1 0 0] x2 + [1]
[0 0 0 0] [0 0 1 0] [1]
[1 1 1 1] [0 1 0 1] [1]
[1 1 0 0] [1 0 1 0] [0]
[insert#1](x1, x2) = [0 1 0 0] x1 + [0 0 0 0] x2 + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 1 0 1] [1 1 1 1] [1]
[0 0 0 0] [1 0 0 0] [1]
[::](x1, x2) = [0 0 0 0] x1 + [0 1 0 0] x2 + [1]
[0 0 0 0] [0 1 0 0] [0]
[1 1 1 1] [0 0 1 1] [0]
[1 0 1 0] [1 0 1 0] [0 0 0
0] [1 1 0 0] [1]
[insert#2](x1, x2, x3, x4) = [0 0 0 1] x1 + [0 0 0 0] x2 + [0 0 0
0] x3 + [0 1 0 0] x4 + [1]
[1 0 0 0] [0 0 0 0] [0 0 0
0] [0 1 0 0] [0]
[1 0 0 0] [1 1 1 1] [1 1 1
1] [0 1 1 1] [1]
[1]
[nil] = [1]
[0]
[0]
[1]
[#false] = [0]
[0]
[1]
[1]
[#true] = [0]
[0]
[1]
[0 1 1 1] [1 0 0 0] [1]
[insertD](x1, x2) = [0 0 0 0] x1 + [0 1 0 0] x2 + [1]
[0 0 0 0] [0 1 0 0] [0]
[1 1 1 1] [0 0 1 1] [0]
[1 0 0 0] [0 1 1 1] [1]
[insertD#1](x1, x2) = [0 1 0 0] x1 + [0 0 0 0] x2 + [1]
[0 1 0 0] [0 0 0 0] [0]
[0 0 1 1] [1 1 1 1] [0]
[1 1 1 1] [0 1 1 1] [0 0 0
0] [1 0 0 0] [0]
[insertD#2](x1, x2, x3, x4) = [0 0 0 1] x1 + [0 0 0 0] x2 + [0 0 0
0] x3 + [0 1 0 0] x4 + [1]
[0 0 0 0] [0 0 0 0] [0 0 0
0] [0 1 0 0] [1]
[0 1 1 0] [1 1 1 1] [1 1 1
1] [0 1 1 1] [0]
[1 0 1 1] [1]
[insertionsort](x1) = [0 1 0 0] x1 + [0]
[0 1 0 1] [0]
[1 1 1 1] [0]
[1 0 1 1] [1]
[insertionsort#1](x1) = [0 1 0 0] x1 + [0]
[0 1 0 1] [0]
[1 1 1 1] [0]
[0 1 1 1] [1]
[insertionsortD](x1) = [0 1 0 0] x1 + [0]
[0 0 1 0] [0]
[0 1 0 1] [0]
[0 1 1 1] [1]
[insertionsortD#1](x1) = [0 1 0 0] x1 + [0]
[0 0 1 0] [0]
[0 1 0 1] [0]
[0]
[#EQ] = [0]
[0]
[0]
[0]
[#GT] = [0]
[0]
[0]
[0]
[#LT] = [0]
[0]
[0]
This order satisfies following ordering constraints
[#abs(#0())] = [3]
[2]
[2]
[2]
> [1]
[0]
[1]
[1]
= [#0()]
[#abs(#neg(@x))] = [1 2 1 0] [2]
[1 1 1 0] @x + [1]
[1 0 1 0] [1]
[1 0 1 0] [1]
> [0 1 0 0] [0]
[0 0 0 0] @x + [0]
[0 0 1 0] [1]
[0 0 1 0] [1]
= [#pos(@x)]
[#abs(#pos(@x))] = [0 1 2 0] [2]
[0 1 1 0] @x + [1]
[0 1 1 0] [1]
[0 1 1 0] [1]
> [0 1 0 0] [0]
[0 0 0 0] @x + [0]
[0 0 1 0] [1]
[0 0 1 0] [1]
= [#pos(@x)]
[#abs(#s(@x))] = [0 3 1 1] [1]
[0 3 1 1] @x + [1]
[0 2 1 1] [1]
[0 2 1 1] [1]
> [0 1 0 0] [0]
[0 0 0 0] @x + [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [#pos(#s(@x))]
[#less(@x, @y)] = [1]
[0]
[0]
[1]
>= [1]
[0]
[0]
[1]
= [#cklt(#compare(@x, @y))]
[#compare(#0(), #0())] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#LT()]
[#compare(#0(), #s(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#LT()]
[#compare(#neg(@x), #0())] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#compare(@y, @x)]
[#compare(#neg(@x), #pos(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#LT()]
[#compare(#pos(@x), #0())] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#GT()]
[#compare(#pos(@x), #pos(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#compare(@x, @y)]
[#compare(#s(@x), #0())] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#compare(@x, @y)]
[#cklt(#EQ())] = [1]
[0]
[0]
[1]
>= [1]
[0]
[0]
[1]
= [#false()]
[#cklt(#GT())] = [1]
[0]
[0]
[1]
>= [1]
[0]
[0]
[1]
= [#false()]
[#cklt(#LT())] = [1]
[0]
[0]
[1]
>= [1]
[0]
[0]
[1]
= [#true()]
[insert(@x, @l)] = [1 1 0 0] [1 0 1 0] [1]
[0 1 0 0] @l + [0 0 0 0] @x + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 1 0 1] [1 1 1 1] [1]
> [1 1 0 0] [1 0 1 0] [0]
[0 1 0 0] @l + [0 0 0 0] @x + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 1 0 1] [1 1 1 1] [1]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [1 0 1 0] [0 0 0 0] [1 1 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[1 1 1 1] [1 1 1 1] [0 1 1 1] [2]
>= [1 0 1 0] [0 0 0 0] [1 1 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[1 1 1 1] [1 1 1 1] [0 1 1 1] [2]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [1 0 1 0] [2]
[0 0 0 0] @x + [2]
[0 0 0 0] [1]
[1 1 1 1] [2]
>= [0 0 0 0] [2]
[0 0 0 0] @x + [2]
[0 0 0 0] [1]
[1 1 1 1] [0]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [1 0 1 0] [0 0 0 0] [1 1 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[1 1 1 1] [1 1 1 1] [0 1 1 1] [2]
>= [0 0 0 0] [0 0 0 0] [1 0 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[1 1 1 1] [1 1 1 1] [0 1 1 1] [0]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [1 0 1 0] [0 0 0 0] [1 1 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[1 1 1 1] [1 1 1 1] [0 1 1 1] [2]
>= [1 0 1 0] [0 0 0 0] [1 1 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[1 1 1 1] [1 1 1 1] [0 1 1 1] [2]
= [::(@y, insert(@x, @ys))]
[insertD(@x, @l)] = [1 0 0 0] [0 1 1 1] [1]
[0 1 0 0] @l + [0 0 0 0] @x + [1]
[0 1 0 0] [0 0 0 0] [0]
[0 0 1 1] [1 1 1 1] [0]
>= [1 0 0 0] [0 1 1 1] [1]
[0 1 0 0] @l + [0 0 0 0] @x + [1]
[0 1 0 0] [0 0 0 0] [0]
[0 0 1 1] [1 1 1 1] [0]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [0 1 1 1] [0 0 0 0] [1 0 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[1 1 1 1] [1 1 1 1] [0 1 1 1] [0]
>= [0 1 1 1] [0 0 0 0] [1 0 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[1 1 1 1] [1 1 1 1] [0 1 1 1] [0]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [0 1 1 1] [2]
[0 0 0 0] @x + [2]
[0 0 0 0] [1]
[1 1 1 1] [0]
>= [0 0 0 0] [2]
[0 0 0 0] @x + [2]
[0 0 0 0] [1]
[1 1 1 1] [0]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [0 1 1 1] [0 0 0 0] [1 0 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[1 1 1 1] [1 1 1 1] [0 1 1 1] [0]
>= [0 0 0 0] [0 0 0 0] [1 0 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[1 1 1 1] [1 1 1 1] [0 1 1 1] [0]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [0 1 1 1] [0 0 0 0] [1 0 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[1 1 1 1] [1 1 1 1] [0 1 1 1] [0]
>= [0 1 1 1] [0 0 0 0] [1 0 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[1 1 1 1] [1 1 1 1] [0 1 1 1] [0]
= [::(@y, insertD(@x, @ys))]
[insertionsort(@l)] = [1 0 1 1] [1]
[0 1 0 0] @l + [0]
[0 1 0 1] [0]
[1 1 1 1] [0]
>= [1 0 1 1] [1]
[0 1 0 0] @l + [0]
[0 1 0 1] [0]
[1 1 1 1] [0]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [1 1 1 1] [1 1 1 1] [2]
[0 0 0 0] @x + [0 1 0 0] @xs + [1]
[1 1 1 1] [0 1 1 1] [1]
[1 1 1 1] [1 2 1 1] [2]
>= [1 0 1 0] [1 1 1 1] [2]
[0 0 0 0] @x + [0 1 0 0] @xs + [1]
[0 0 0 0] [0 1 0 1] [1]
[1 1 1 1] [1 2 1 1] [1]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [2]
[1]
[1]
[2]
> [1]
[1]
[0]
[0]
= [nil()]
[insertionsortD(@l)] = [0 1 1 1] [1]
[0 1 0 0] @l + [0]
[0 0 1 0] [0]
[0 1 0 1] [0]
>= [0 1 1 1] [1]
[0 1 0 0] @l + [0]
[0 0 1 0] [0]
[0 1 0 1] [0]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [1 1 1 1] [0 2 1 1] [2]
[0 0 0 0] @x + [0 1 0 0] @xs + [1]
[0 0 0 0] [0 1 0 0] [0]
[1 1 1 1] [0 1 1 1] [1]
>= [0 1 1 1] [0 1 1 1] [2]
[0 0 0 0] @x + [0 1 0 0] @xs + [1]
[0 0 0 0] [0 1 0 0] [0]
[1 1 1 1] [0 1 1 1] [0]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [2]
[1]
[0]
[1]
> [1]
[1]
[0]
[0]
= [nil()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys)) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 4' to
orient following rules strictly.
Trs:
{ insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^3)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(#cklt) = {1}, Uargs(insert) = {2}, Uargs(::) = {2},
Uargs(insert#2) = {1}, Uargs(insertD) = {2}, Uargs(insertD#2) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA) and not(IDA(3)).
[0]
[#0] = [0]
[1]
[1]
[1 1 0 0] [1]
[#abs](x1) = [1 1 1 1] x1 + [0]
[1 0 0 0] [1]
[1 1 0 1] [0]
[0 0 0 0] [1]
[#neg](x1) = [1 1 0 1] x1 + [1]
[0 0 0 0] [1]
[0 0 0 0] [0]
[1 0 0 1] [1]
[#pos](x1) = [0 1 0 1] x1 + [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
[1 0 0 1] [1]
[#s](x1) = [0 1 0 0] x1 + [0]
[0 0 1 0] [1]
[0 0 0 0] [0]
[1]
[#less](x1, x2) = [1]
[0]
[1]
[1]
[#compare](x1, x2) = [0]
[1]
[1]
[1 0 0 0] [0]
[#cklt](x1) = [0 1 1 0] x1 + [0]
[0 1 0 0] [0]
[0 0 1 0] [0]
[1 1 0 0] [1 0 1 0] [1]
[insert](x1, x2) = [0 0 1 1] x1 + [0 1 1 0] x2 + [0]
[0 0 0 0] [0 0 1 0] [1]
[0 0 0 0] [0 0 0 1] [1]
[1 0 1 0] [1 1 0 0] [1]
[insert#1](x1, x2) = [0 1 1 0] x1 + [0 0 1 1] x2 + [0]
[0 0 1 0] [0 0 0 0] [1]
[0 0 0 1] [0 0 0 0] [1]
[1 1 0 0] [1 0 0 0] [0]
[::](x1, x2) = [0 0 1 1] x1 + [0 1 0 1] x2 + [0]
[0 0 0 0] [0 0 1 0] [1]
[0 0 0 0] [0 0 1 0] [1]
[1 0 1 1] [1 1 0 0] [1 1 0
0] [1 0 1 0] [0]
[insert#2](x1, x2, x3, x4) = [0 0 1 0] x1 + [0 0 1 1] x2 + [0 0 1
1] x3 + [0 1 1 1] x4 + [1]
[0 0 1 1] [0 0 0 0] [0 0 0
0] [0 0 1 0] [1]
[0 1 0 1] [0 0 0 0] [0 0 0
0] [0 0 1 0] [0]
[0]
[nil] = [0]
[0]
[0]
[0]
[#false] = [1]
[0]
[1]
[1]
[#true] = [1]
[0]
[1]
[1 1 0 0] [1 0 1 0] [1]
[insertD](x1, x2) = [1 1 1 1] x1 + [0 1 1 0] x2 + [0]
[0 0 0 0] [0 0 1 0] [1]
[0 0 0 0] [0 0 0 1] [1]
[1 0 1 0] [1 1 0 0] [1]
[insertD#1](x1, x2) = [0 1 1 0] x1 + [1 1 1 1] x2 + [0]
[0 0 1 0] [0 0 0 0] [1]
[0 0 0 1] [0 0 0 0] [1]
[1 0 1 1] [1 1 0 0] [1 1 0
0] [1 0 1 0] [0]
[insertD#2](x1, x2, x3, x4) = [0 1 1 0] x1 + [1 1 1 1] x2 + [0 0 1
1] x3 + [0 1 1 1] x4 + [0]
[0 1 1 1] [0 0 0 0] [0 0 0
0] [0 0 1 0] [0]
[0 1 0 1] [0 0 0 0] [0 0 0
0] [0 0 1 0] [0]
[1 1 0 1] [0]
[insertionsort](x1) = [1 1 0 1] x1 + [0]
[0 0 1 0] [0]
[0 1 0 1] [0]
[1 1 0 1] [0]
[insertionsort#1](x1) = [1 1 0 1] x1 + [0]
[0 0 1 0] [0]
[0 1 0 1] [0]
[1 1 0 1] [0]
[insertionsortD](x1) = [1 1 1 1] x1 + [1]
[0 0 1 0] [0]
[0 0 1 0] [0]
[1 1 0 1] [0]
[insertionsortD#1](x1) = [1 1 1 1] x1 + [1]
[0 0 1 0] [0]
[0 0 1 0] [0]
[0]
[#EQ] = [0]
[1]
[1]
[0]
[#GT] = [0]
[1]
[1]
[1]
[#LT] = [0]
[1]
[0]
This order satisfies following ordering constraints
[#abs(#0())] = [1]
[2]
[1]
[1]
> [0]
[0]
[1]
[1]
= [#0()]
[#abs(#neg(@x))] = [1 1 0 1] [3]
[1 1 0 1] @x + [3]
[0 0 0 0] [2]
[1 1 0 1] [2]
> [1 0 0 1] [1]
[0 1 0 1] @x + [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [#pos(@x)]
[#abs(#pos(@x))] = [1 1 0 2] [2]
[1 1 0 2] @x + [3]
[1 0 0 1] [2]
[1 1 0 2] [2]
> [1 0 0 1] [1]
[0 1 0 1] @x + [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [#pos(@x)]
[#abs(#s(@x))] = [1 1 0 1] [2]
[1 1 1 1] @x + [2]
[1 0 0 1] [2]
[1 1 0 1] [1]
>= [1 0 0 1] [2]
[0 1 0 0] @x + [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [#pos(#s(@x))]
[#less(@x, @y)] = [1]
[1]
[0]
[1]
>= [1]
[1]
[0]
[1]
= [#cklt(#compare(@x, @y))]
[#compare(#0(), #0())] = [1]
[0]
[1]
[1]
> [0]
[0]
[1]
[1]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [1]
[0]
[1]
[1]
> [0]
[0]
[1]
[1]
= [#GT()]
[#compare(#0(), #pos(@y))] = [1]
[0]
[1]
[1]
>= [1]
[0]
[1]
[0]
= [#LT()]
[#compare(#0(), #s(@y))] = [1]
[0]
[1]
[1]
>= [1]
[0]
[1]
[0]
= [#LT()]
[#compare(#neg(@x), #0())] = [1]
[0]
[1]
[1]
>= [1]
[0]
[1]
[0]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [1]
[0]
[1]
[1]
>= [1]
[0]
[1]
[1]
= [#compare(@y, @x)]
[#compare(#neg(@x), #pos(@y))] = [1]
[0]
[1]
[1]
>= [1]
[0]
[1]
[0]
= [#LT()]
[#compare(#pos(@x), #0())] = [1]
[0]
[1]
[1]
> [0]
[0]
[1]
[1]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [1]
[0]
[1]
[1]
> [0]
[0]
[1]
[1]
= [#GT()]
[#compare(#pos(@x), #pos(@y))] = [1]
[0]
[1]
[1]
>= [1]
[0]
[1]
[1]
= [#compare(@x, @y)]
[#compare(#s(@x), #0())] = [1]
[0]
[1]
[1]
> [0]
[0]
[1]
[1]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [1]
[0]
[1]
[1]
>= [1]
[0]
[1]
[1]
= [#compare(@x, @y)]
[#cklt(#EQ())] = [0]
[1]
[0]
[1]
>= [0]
[1]
[0]
[1]
= [#false()]
[#cklt(#GT())] = [0]
[1]
[0]
[1]
>= [0]
[1]
[0]
[1]
= [#false()]
[#cklt(#LT())] = [1]
[1]
[0]
[1]
>= [1]
[1]
[0]
[1]
= [#true()]
[insert(@x, @l)] = [1 0 1 0] [1 1 0 0] [1]
[0 1 1 0] @l + [0 0 1 1] @x + [0]
[0 0 1 0] [0 0 0 0] [1]
[0 0 0 1] [0 0 0 0] [1]
>= [1 0 1 0] [1 1 0 0] [1]
[0 1 1 0] @l + [0 0 1 1] @x + [0]
[0 0 1 0] [0 0 0 0] [1]
[0 0 0 1] [0 0 0 0] [1]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [1 1 0 0] [1 1 0 0] [1 0 1 0] [2]
[0 0 1 1] @x + [0 0 1 1] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
>= [1 1 0 0] [1 1 0 0] [1 0 1 0] [2]
[0 0 1 1] @x + [0 0 1 1] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [1 1 0 0] [1]
[0 0 1 1] @x + [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
> [1 1 0 0] [0]
[0 0 1 1] @x + [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [1 1 0 0] [1 1 0 0] [1 0 1 0] [1]
[0 0 1 1] @x + [0 0 1 1] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
> [1 1 0 0] [1 1 0 0] [1 0 0 0] [0]
[0 0 1 1] @x + [0 0 1 1] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [1 1 0 0] [1 1 0 0] [1 0 1 0] [2]
[0 0 1 1] @x + [0 0 1 1] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
> [1 1 0 0] [1 1 0 0] [1 0 1 0] [1]
[0 0 1 1] @x + [0 0 1 1] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
= [::(@y, insert(@x, @ys))]
[insertD(@x, @l)] = [1 0 1 0] [1 1 0 0] [1]
[0 1 1 0] @l + [1 1 1 1] @x + [0]
[0 0 1 0] [0 0 0 0] [1]
[0 0 0 1] [0 0 0 0] [1]
>= [1 0 1 0] [1 1 0 0] [1]
[0 1 1 0] @l + [1 1 1 1] @x + [0]
[0 0 1 0] [0 0 0 0] [1]
[0 0 0 1] [0 0 0 0] [1]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [1 1 0 0] [1 1 0 0] [1 0 1 0] [2]
[1 1 1 1] @x + [0 0 1 1] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
>= [1 1 0 0] [1 1 0 0] [1 0 1 0] [2]
[1 1 1 1] @x + [0 0 1 1] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [1 1 0 0] [1]
[1 1 1 1] @x + [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
> [1 1 0 0] [0]
[0 0 1 1] @x + [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [1 1 0 0] [1 1 0 0] [1 0 1 0] [1]
[1 1 1 1] @x + [0 0 1 1] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
> [1 1 0 0] [1 1 0 0] [1 0 0 0] [0]
[0 0 1 1] @x + [0 0 1 1] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [1 1 0 0] [1 1 0 0] [1 0 1 0] [2]
[1 1 1 1] @x + [0 0 1 1] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
> [1 1 0 0] [1 1 0 0] [1 0 1 0] [1]
[1 1 1 1] @x + [0 0 1 1] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
= [::(@y, insertD(@x, @ys))]
[insertionsort(@l)] = [1 1 0 1] [0]
[1 1 0 1] @l + [0]
[0 0 1 0] [0]
[0 1 0 1] [0]
>= [1 1 0 1] [0]
[1 1 0 1] @l + [0]
[0 0 1 0] [0]
[0 1 0 1] [0]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] @x + [1 1 1 1] @xs + [1]
[0 0 0 0] [0 0 1 0] [1]
[0 0 1 1] [0 1 1 1] [1]
>= [1 1 0 0] [1 1 1 1] [1]
[0 0 1 1] @x + [1 1 1 1] @xs + [0]
[0 0 0 0] [0 0 1 0] [1]
[0 0 0 0] [0 1 0 1] [1]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [nil()]
[insertionsortD(@l)] = [1 1 0 1] [0]
[1 1 1 1] @l + [1]
[0 0 1 0] [0]
[0 0 1 0] [0]
>= [1 1 0 1] [0]
[1 1 1 1] @l + [1]
[0 0 1 0] [0]
[0 0 1 0] [0]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] @x + [1 1 2 1] @xs + [3]
[0 0 0 0] [0 0 1 0] [1]
[0 0 0 0] [0 0 1 0] [1]
>= [1 1 0 0] [1 1 1 1] [1]
[1 1 1 1] @x + [1 1 2 1] @xs + [1]
[0 0 0 0] [0 0 1 0] [1]
[0 0 0 0] [0 0 1 0] [1]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [0]
[1]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [nil()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 4' to
orient following rules strictly.
Trs:
{ insert#1(::(@y, @ys), @x) ->
insert#2(#less(@y, @x), @x, @y, @ys) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^3)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(#cklt) = {1}, Uargs(insert) = {2}, Uargs(::) = {2},
Uargs(insert#2) = {1}, Uargs(insertD) = {2}, Uargs(insertD#2) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA) and not(IDA(3)).
[1]
[#0] = [0]
[1]
[1]
[1 0 0 0] [0]
[#abs](x1) = [0 1 1 0] x1 + [0]
[1 1 1 1] [0]
[1 1 0 0] [0]
[1 0 0 0] [0]
[#neg](x1) = [0 0 0 0] x1 + [0]
[0 1 1 1] [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
[#pos](x1) = [0 0 1 0] x1 + [0]
[1 1 0 0] [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
[#s](x1) = [1 0 0 0] x1 + [0]
[1 0 0 0] [0]
[0 0 0 1] [0]
[0 0 0 0] [1]
[#less](x1, x2) = [1 0 0 0] x2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
[0]
[#compare](x1, x2) = [0]
[0]
[0]
[1 0 1 0] [1]
[#cklt](x1) = [0 0 0 0] x1 + [1]
[1 1 1 1] [0]
[0 0 0 0] [1]
[1 0 0 1] [1 0 0 1] [1]
[insert](x1, x2) = [1 0 1 1] x1 + [0 1 1 0] x2 + [1]
[0 0 0 0] [0 0 0 1] [0]
[0 0 0 0] [0 0 0 1] [1]
[1 0 0 1] [1 0 0 1] [1]
[insert#1](x1, x2) = [0 1 1 0] x1 + [1 0 1 1] x2 + [1]
[0 0 0 1] [0 0 0 0] [0]
[0 0 0 1] [0 0 0 0] [1]
[0 0 0 1] [1 0 0 0] [1]
[::](x1, x2) = [1 0 1 0] x1 + [0 1 1 0] x2 + [0]
[0 0 0 0] [0 0 0 1] [0]
[0 0 0 0] [0 0 0 1] [1]
[1 0 1 1] [1 0 0 1] [0 0 0
1] [1 0 0 1] [0]
[insert#2](x1, x2, x3, x4) = [0 0 0 0] x1 + [1 0 1 1] x2 + [1 0 1
0] x3 + [0 1 1 1] x4 + [1]
[0 0 0 0] [0 0 0 0] [0 0 0
0] [0 0 0 1] [1]
[1 0 1 0] [0 0 0 0] [0 0 0
0] [0 0 0 1] [1]
[1]
[nil] = [0]
[0]
[0]
[1]
[#false] = [1]
[0]
[1]
[1]
[#true] = [0]
[0]
[1]
[1 0 1 1] [1 0 0 0] [1]
[insertD](x1, x2) = [1 0 1 0] x1 + [0 1 0 1] x2 + [1]
[0 0 0 0] [0 0 1 0] [1]
[0 0 0 0] [0 0 0 1] [1]
[1 0 0 0] [1 0 1 1] [1]
[insertD#1](x1, x2) = [0 1 0 1] x1 + [1 0 1 0] x2 + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 0 0 1] [0 0 0 0] [1]
[1 0 1 0] [1 0 1 1] [0 0 0
1] [1 0 0 0] [1]
[insertD#2](x1, x2, x3, x4) = [0 0 0 1] x1 + [1 0 1 0] x2 + [1 0 1
0] x3 + [0 1 1 1] x4 + [1]
[1 0 0 0] [0 0 0 0] [0 0 0
0] [0 0 0 1] [0]
[1 0 0 0] [0 0 0 0] [0 0 0
0] [0 0 0 1] [1]
[1 1 1 0] [0]
[insertionsort](x1) = [1 1 1 0] x1 + [0]
[0 0 0 1] [0]
[0 0 0 1] [0]
[1 1 1 0] [0]
[insertionsort#1](x1) = [1 1 1 0] x1 + [0]
[0 0 0 1] [0]
[0 0 0 1] [0]
[1 1 1 1] [1]
[insertionsortD](x1) = [1 1 1 0] x1 + [0]
[1 1 1 0] [0]
[0 0 0 1] [0]
[1 1 1 1] [1]
[insertionsortD#1](x1) = [1 1 1 0] x1 + [0]
[1 1 0 0] [0]
[0 0 0 1] [0]
[0]
[#EQ] = [0]
[0]
[0]
[0]
[#GT] = [0]
[0]
[0]
[0]
[#LT] = [0]
[0]
[0]
This order satisfies following ordering constraints
[#abs(#0())] = [1]
[1]
[3]
[1]
>= [1]
[0]
[1]
[1]
= [#0()]
[#abs(#neg(@x))] = [1 0 0 0] [0]
[0 1 1 1] @x + [0]
[1 1 1 1] [0]
[1 0 0 0] [0]
>= [0 0 0 0] [0]
[0 0 1 0] @x + [0]
[1 1 0 0] [0]
[0 0 0 0] [0]
= [#pos(@x)]
[#abs(#pos(@x))] = [0 0 0 0] [0]
[1 1 1 0] @x + [0]
[1 1 1 0] [0]
[0 0 1 0] [0]
>= [0 0 0 0] [0]
[0 0 1 0] @x + [0]
[1 1 0 0] [0]
[0 0 0 0] [0]
= [#pos(@x)]
[#abs(#s(@x))] = [0 0 0 0] [0]
[2 0 0 0] @x + [0]
[2 0 0 1] [0]
[1 0 0 0] [0]
>= [0 0 0 0] [0]
[1 0 0 0] @x + [0]
[1 0 0 0] [0]
[0 0 0 0] [0]
= [#pos(#s(@x))]
[#less(@x, @y)] = [0 0 0 0] [1]
[1 0 0 0] @y + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
>= [1]
[1]
[0]
[1]
= [#cklt(#compare(@x, @y))]
[#compare(#0(), #0())] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#LT()]
[#compare(#0(), #s(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#LT()]
[#compare(#neg(@x), #0())] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#compare(@y, @x)]
[#compare(#neg(@x), #pos(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#LT()]
[#compare(#pos(@x), #0())] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#GT()]
[#compare(#pos(@x), #pos(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#compare(@x, @y)]
[#compare(#s(@x), #0())] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#compare(@x, @y)]
[#cklt(#EQ())] = [1]
[1]
[0]
[1]
>= [1]
[1]
[0]
[1]
= [#false()]
[#cklt(#GT())] = [1]
[1]
[0]
[1]
>= [1]
[1]
[0]
[1]
= [#false()]
[#cklt(#LT())] = [1]
[1]
[0]
[1]
>= [1]
[0]
[0]
[1]
= [#true()]
[insert(@x, @l)] = [1 0 0 1] [1 0 0 1] [1]
[0 1 1 0] @l + [1 0 1 1] @x + [1]
[0 0 0 1] [0 0 0 0] [0]
[0 0 0 1] [0 0 0 0] [1]
>= [1 0 0 1] [1 0 0 1] [1]
[0 1 1 0] @l + [1 0 1 1] @x + [1]
[0 0 0 1] [0 0 0 0] [0]
[0 0 0 1] [0 0 0 0] [1]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [1 0 0 1] [0 0 0 1] [1 0 0 1] [3]
[1 0 1 1] @x + [1 0 1 0] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
> [1 0 0 1] [0 0 0 1] [1 0 0 1] [2]
[1 0 1 1] @x + [1 0 1 0] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [1 0 0 1] [2]
[1 0 1 1] @x + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
>= [0 0 0 1] [2]
[1 0 1 0] @x + [0]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [1 0 0 1] [0 0 0 1] [1 0 0 1] [2]
[1 0 1 1] @x + [1 0 1 0] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
>= [0 0 0 1] [0 0 0 1] [1 0 0 0] [2]
[1 0 1 0] @x + [1 0 1 0] @y + [0 1 1 1] @ys + [0]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [1 0 0 1] [0 0 0 1] [1 0 0 1] [2]
[1 0 1 1] @x + [1 0 1 0] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
>= [1 0 0 1] [0 0 0 1] [1 0 0 1] [2]
[1 0 1 1] @x + [1 0 1 0] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
= [::(@y, insert(@x, @ys))]
[insertD(@x, @l)] = [1 0 0 0] [1 0 1 1] [1]
[0 1 0 1] @l + [1 0 1 0] @x + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 0 0 1] [0 0 0 0] [1]
>= [1 0 0 0] [1 0 1 1] [1]
[0 1 0 1] @l + [1 0 1 0] @x + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 0 0 1] [0 0 0 0] [1]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [1 0 1 1] [0 0 0 1] [1 0 0 0] [2]
[1 0 1 0] @x + [1 0 1 0] @y + [0 1 1 1] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
>= [1 0 1 1] [0 0 0 1] [1 0 0 0] [2]
[1 0 1 0] @x + [1 0 1 0] @y + [0 1 1 1] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [1 0 1 1] [2]
[1 0 1 0] @x + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
>= [0 0 0 1] [2]
[1 0 1 0] @x + [0]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [1 0 1 1] [0 0 0 1] [1 0 0 0] [2]
[1 0 1 0] @x + [1 0 1 0] @y + [0 1 1 1] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
>= [0 0 0 1] [0 0 0 1] [1 0 0 0] [2]
[1 0 1 0] @x + [1 0 1 0] @y + [0 1 1 1] @ys + [0]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [1 0 1 1] [0 0 0 1] [1 0 0 0] [2]
[1 0 1 0] @x + [1 0 1 0] @y + [0 1 1 1] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
>= [1 0 1 1] [0 0 0 1] [1 0 0 0] [2]
[1 0 1 0] @x + [1 0 1 0] @y + [0 1 1 1] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
= [::(@y, insertD(@x, @ys))]
[insertionsort(@l)] = [1 1 1 0] [0]
[1 1 1 0] @l + [0]
[0 0 0 1] [0]
[0 0 0 1] [0]
>= [1 1 1 0] [0]
[1 1 1 0] @l + [0]
[0 0 0 1] [0]
[0 0 0 1] [0]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [1 0 1 1] [1 1 1 1] [1]
[1 0 1 1] @x + [1 1 1 1] @xs + [1]
[0 0 0 0] [0 0 0 1] [1]
[0 0 0 0] [0 0 0 1] [1]
>= [1 0 0 1] [1 1 1 1] [1]
[1 0 1 1] @x + [1 1 1 1] @xs + [1]
[0 0 0 0] [0 0 0 1] [0]
[0 0 0 0] [0 0 0 1] [1]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [1]
[1]
[0]
[0]
>= [1]
[0]
[0]
[0]
= [nil()]
[insertionsortD(@l)] = [1 1 1 1] [1]
[1 1 1 0] @l + [0]
[1 1 1 0] [0]
[0 0 0 1] [0]
>= [1 1 1 1] [1]
[1 1 1 0] @l + [0]
[1 1 0 0] [0]
[0 0 0 1] [0]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [1 0 1 1] [1 1 1 2] [3]
[1 0 1 1] @x + [1 1 1 1] @xs + [1]
[1 0 1 1] [1 1 1 0] [1]
[0 0 0 0] [0 0 0 1] [1]
> [1 0 1 1] [1 1 1 1] [2]
[1 0 1 0] @x + [1 1 1 1] @xs + [1]
[0 0 0 0] [1 1 1 0] [1]
[0 0 0 0] [0 0 0 1] [1]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [2]
[1]
[1]
[0]
> [1]
[0]
[0]
[0]
= [nil()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 4' to
orient following rules strictly.
Trs:
{ insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^3)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(#cklt) = {1}, Uargs(insert) = {2}, Uargs(::) = {2},
Uargs(insert#2) = {1}, Uargs(insertD) = {2}, Uargs(insertD#2) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA) and not(IDA(3)).
[0]
[#0] = [0]
[0]
[0]
[1 1 1 0] [0]
[#abs](x1) = [1 1 0 0] x1 + [0]
[1 0 1 1] [0]
[0 0 0 1] [0]
[0 1 0 0] [0]
[#neg](x1) = [1 0 1 0] x1 + [0]
[0 0 0 1] [0]
[0 0 0 0] [0]
[1 0 1 1] [0]
[#pos](x1) = [0 1 0 0] x1 + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
[0 0 1 0] [0]
[#s](x1) = [0 1 0 0] x1 + [0]
[0 0 1 0] [0]
[0 0 0 0] [0]
[1]
[#less](x1, x2) = [0]
[0]
[0]
[0]
[#compare](x1, x2) = [1]
[0]
[1]
[1 0 1 1] [0]
[#cklt](x1) = [0 0 0 0] x1 + [0]
[0 0 0 0] [0]
[0 0 1 0] [0]
[1 1 1 1] [1 0 0 0] [1]
[insert](x1, x2) = [1 1 1 1] x1 + [0 1 1 0] x2 + [1]
[0 0 0 0] [0 0 0 1] [1]
[0 0 0 0] [0 0 0 1] [1]
[1 0 0 0] [1 1 1 1] [1]
[insert#1](x1, x2) = [0 1 1 0] x1 + [1 1 1 1] x2 + [1]
[0 0 0 1] [0 0 0 0] [1]
[0 0 0 1] [0 0 0 0] [1]
[0 0 0 0] [1 0 0 0] [0]
[::](x1, x2) = [1 1 1 1] x1 + [0 1 1 0] x2 + [0]
[0 0 0 0] [0 0 0 1] [1]
[0 0 0 0] [0 0 0 1] [1]
[1 0 1 1] [1 1 1 1] [0 0 0
0] [1 0 0 0] [0]
[insert#2](x1, x2, x3, x4) = [1 0 0 0] x1 + [1 1 1 1] x2 + [1 1 1
1] x3 + [0 1 1 1] x4 + [1]
[1 1 0 0] [0 0 0 0] [0 0 0
0] [0 0 0 1] [1]
[1 0 0 0] [0 0 0 0] [0 0 0
0] [0 0 0 1] [1]
[1]
[nil] = [0]
[0]
[0]
[1]
[#false] = [0]
[0]
[0]
[1]
[#true] = [0]
[0]
[0]
[1 1 1 0] [1 0 0 1] [1]
[insertD](x1, x2) = [1 1 1 1] x1 + [0 1 0 1] x2 + [1]
[0 0 0 0] [0 0 1 0] [1]
[0 0 0 0] [0 0 0 1] [1]
[1 0 0 1] [1 1 1 0] [1]
[insertD#1](x1, x2) = [0 1 0 1] x1 + [1 1 1 1] x2 + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 0 0 1] [0 0 0 0] [1]
[1 1 1 1] [1 1 1 0] [0 0 0
0] [1 0 0 1] [0]
[insertD#2](x1, x2, x3, x4) = [1 0 0 0] x1 + [1 1 1 1] x2 + [1 1 1
1] x3 + [0 1 1 1] x4 + [1]
[1 0 0 0] [0 0 0 0] [0 0 0
0] [0 0 0 1] [1]
[1 0 0 0] [0 0 0 0] [0 0 0
0] [0 0 0 1] [1]
[1 1 0 1] [0]
[insertionsort](x1) = [1 1 1 1] x1 + [0]
[0 0 0 1] [1]
[0 0 0 1] [1]
[1 1 0 1] [0]
[insertionsort#1](x1) = [1 1 1 1] x1 + [0]
[0 0 0 1] [1]
[0 0 0 1] [1]
[1 1 1 0] [0]
[insertionsortD](x1) = [1 1 1 1] x1 + [0]
[1 1 1 1] [0]
[0 0 0 1] [0]
[1 1 1 0] [0]
[insertionsortD#1](x1) = [1 1 1 1] x1 + [0]
[1 1 1 1] [0]
[0 0 0 1] [0]
[0]
[#EQ] = [0]
[0]
[1]
[0]
[#GT] = [0]
[0]
[1]
[0]
[#LT] = [1]
[0]
[1]
This order satisfies following ordering constraints
[#abs(#0())] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [#0()]
[#abs(#neg(@x))] = [1 1 1 1] [0]
[1 1 1 0] @x + [0]
[0 1 0 1] [0]
[0 0 0 0] [0]
>= [1 0 1 1] [0]
[0 1 0 0] @x + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [#pos(@x)]
[#abs(#pos(@x))] = [1 1 1 1] [0]
[1 1 1 1] @x + [0]
[1 0 1 1] [0]
[0 0 0 0] [0]
>= [1 0 1 1] [0]
[0 1 0 0] @x + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [#pos(@x)]
[#abs(#s(@x))] = [0 1 2 0] [0]
[0 1 1 0] @x + [0]
[0 0 2 0] [0]
[0 0 0 0] [0]
>= [0 0 2 0] [0]
[0 1 0 0] @x + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [#pos(#s(@x))]
[#less(@x, @y)] = [1]
[0]
[0]
[0]
>= [1]
[0]
[0]
[0]
= [#cklt(#compare(@x, @y))]
[#compare(#0(), #0())] = [0]
[1]
[0]
[1]
>= [0]
[0]
[0]
[1]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [0]
[1]
[0]
[1]
>= [0]
[0]
[0]
[1]
= [#GT()]
[#compare(#0(), #pos(@y))] = [0]
[1]
[0]
[1]
>= [0]
[1]
[0]
[1]
= [#LT()]
[#compare(#0(), #s(@y))] = [0]
[1]
[0]
[1]
>= [0]
[1]
[0]
[1]
= [#LT()]
[#compare(#neg(@x), #0())] = [0]
[1]
[0]
[1]
>= [0]
[1]
[0]
[1]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [0]
[1]
[0]
[1]
>= [0]
[1]
[0]
[1]
= [#compare(@y, @x)]
[#compare(#neg(@x), #pos(@y))] = [0]
[1]
[0]
[1]
>= [0]
[1]
[0]
[1]
= [#LT()]
[#compare(#pos(@x), #0())] = [0]
[1]
[0]
[1]
>= [0]
[0]
[0]
[1]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [0]
[1]
[0]
[1]
>= [0]
[0]
[0]
[1]
= [#GT()]
[#compare(#pos(@x), #pos(@y))] = [0]
[1]
[0]
[1]
>= [0]
[1]
[0]
[1]
= [#compare(@x, @y)]
[#compare(#s(@x), #0())] = [0]
[1]
[0]
[1]
>= [0]
[0]
[0]
[1]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [0]
[1]
[0]
[1]
>= [0]
[1]
[0]
[1]
= [#compare(@x, @y)]
[#cklt(#EQ())] = [1]
[0]
[0]
[0]
>= [1]
[0]
[0]
[0]
= [#false()]
[#cklt(#GT())] = [1]
[0]
[0]
[0]
>= [1]
[0]
[0]
[0]
= [#false()]
[#cklt(#LT())] = [1]
[0]
[0]
[0]
>= [1]
[0]
[0]
[0]
= [#true()]
[insert(@x, @l)] = [1 0 0 0] [1 1 1 1] [1]
[0 1 1 0] @l + [1 1 1 1] @x + [1]
[0 0 0 1] [0 0 0 0] [1]
[0 0 0 1] [0 0 0 0] [1]
>= [1 0 0 0] [1 1 1 1] [1]
[0 1 1 0] @l + [1 1 1 1] @x + [1]
[0 0 0 1] [0 0 0 0] [1]
[0 0 0 1] [0 0 0 0] [1]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [1 1 1 1] [0 0 0 0] [1 0 0 0] [1]
[1 1 1 1] @x + [1 1 1 1] @y + [0 1 1 1] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
>= [1 1 1 1] [0 0 0 0] [1 0 0 0] [1]
[1 1 1 1] @x + [1 1 1 1] @y + [0 1 1 1] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [1 1 1 1] [2]
[1 1 1 1] @x + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
> [0 0 0 0] [1]
[1 1 1 1] @x + [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [1 1 1 1] [0 0 0 0] [1 0 0 0] [1]
[1 1 1 1] @x + [1 1 1 1] @y + [0 1 1 1] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
> [0 0 0 0] [0 0 0 0] [1 0 0 0] [0]
[1 1 1 1] @x + [1 1 1 1] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [1 1 1 1] [0 0 0 0] [1 0 0 0] [1]
[1 1 1 1] @x + [1 1 1 1] @y + [0 1 1 1] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
>= [1 1 1 1] [0 0 0 0] [1 0 0 0] [1]
[1 1 1 1] @x + [1 1 1 1] @y + [0 1 1 1] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
= [::(@y, insert(@x, @ys))]
[insertD(@x, @l)] = [1 0 0 1] [1 1 1 0] [1]
[0 1 0 1] @l + [1 1 1 1] @x + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 0 0 1] [0 0 0 0] [1]
>= [1 0 0 1] [1 1 1 0] [1]
[0 1 0 1] @l + [1 1 1 1] @x + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 0 0 1] [0 0 0 0] [1]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [1 1 1 0] [0 0 0 0] [1 0 0 1] [2]
[1 1 1 1] @x + [1 1 1 1] @y + [0 1 1 1] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
> [1 1 1 0] [0 0 0 0] [1 0 0 1] [1]
[1 1 1 1] @x + [1 1 1 1] @y + [0 1 1 1] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [1 1 1 0] [2]
[1 1 1 1] @x + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
> [0 0 0 0] [1]
[1 1 1 1] @x + [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [1 1 1 0] [0 0 0 0] [1 0 0 1] [1]
[1 1 1 1] @x + [1 1 1 1] @y + [0 1 1 1] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
> [0 0 0 0] [0 0 0 0] [1 0 0 0] [0]
[1 1 1 1] @x + [1 1 1 1] @y + [0 1 1 1] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [1 1 1 0] [0 0 0 0] [1 0 0 1] [1]
[1 1 1 1] @x + [1 1 1 1] @y + [0 1 1 1] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
>= [1 1 1 0] [0 0 0 0] [1 0 0 1] [1]
[1 1 1 1] @x + [1 1 1 1] @y + [0 1 1 1] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
[0 0 0 0] [0 0 0 0] [0 0 0 1] [2]
= [::(@y, insertD(@x, @ys))]
[insertionsort(@l)] = [1 1 0 1] [0]
[1 1 1 1] @l + [0]
[0 0 0 1] [1]
[0 0 0 1] [1]
>= [1 1 0 1] [0]
[1 1 1 1] @l + [0]
[0 0 0 1] [1]
[0 0 0 1] [1]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] @x + [1 1 1 2] @xs + [2]
[0 0 0 0] [0 0 0 1] [2]
[0 0 0 0] [0 0 0 1] [2]
>= [1 1 1 1] [1 1 0 1] [1]
[1 1 1 1] @x + [1 1 1 2] @xs + [2]
[0 0 0 0] [0 0 0 1] [2]
[0 0 0 0] [0 0 0 1] [2]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [1]
[1]
[1]
[1]
>= [1]
[0]
[0]
[0]
= [nil()]
[insertionsortD(@l)] = [1 1 1 0] [0]
[1 1 1 1] @l + [0]
[1 1 1 1] [0]
[0 0 0 1] [0]
>= [1 1 1 0] [0]
[1 1 1 1] @l + [0]
[1 1 1 1] [0]
[0 0 0 1] [0]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] @x + [1 1 1 2] @xs + [2]
[1 1 1 1] [1 1 1 2] [2]
[0 0 0 0] [0 0 0 1] [1]
>= [1 1 1 0] [1 1 1 1] [1]
[1 1 1 1] @x + [1 1 1 2] @xs + [1]
[0 0 0 0] [1 1 1 1] [1]
[0 0 0 0] [0 0 0 1] [1]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [1]
[1]
[1]
[0]
>= [1]
[0]
[0]
[0]
= [nil()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, insertD(@x, @l) -> insertD#1(@l, @x) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 4' to
orient following rules strictly.
Trs: { insertD(@x, @l) -> insertD#1(@l, @x) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^3)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(#cklt) = {1}, Uargs(insert) = {2}, Uargs(::) = {2},
Uargs(insert#2) = {1}, Uargs(insertD) = {2}, Uargs(insertD#2) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA) and not(IDA(3)).
[0]
[#0] = [1]
[1]
[0]
[1 1 0 0] [1]
[#abs](x1) = [1 1 1 1] x1 + [1]
[1 0 1 0] [1]
[1 1 1 0] [0]
[1 0 1 0] [0]
[#neg](x1) = [0 1 0 0] x1 + [0]
[0 0 0 0] [0]
[0 0 1 1] [0]
[1 0 0 0] [0]
[#pos](x1) = [0 1 0 1] x1 + [1]
[0 0 1 0] [1]
[0 0 1 0] [0]
[0 0 0 0] [0]
[#s](x1) = [0 0 1 1] x1 + [1]
[0 0 1 0] [0]
[1 1 1 0] [0]
[0 0 0 0] [0 0 0 0] [0]
[#less](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [1]
[0 0 0 0] [0 0 0 0] [1]
[0 1 1 1] [0 1 0 1] [0]
[0 0 0 0] [0 0 0 0] [0]
[#compare](x1, x2) = [1 1 0 1] x1 + [1 1 0 1] x2 + [0]
[0 0 0 0] [0 0 0 0] [1]
[0 1 1 1] [0 1 0 1] [0]
[1 0 0 0] [0]
[#cklt](x1) = [0 0 0 0] x1 + [1]
[0 0 1 0] [0]
[0 0 0 1] [0]
[0 0 0 1] [1 0 1 0] [1]
[insert](x1, x2) = [0 0 0 0] x1 + [0 0 0 1] x2 + [1]
[0 0 0 0] [0 0 1 0] [1]
[0 0 0 0] [0 1 1 0] [0]
[1 0 1 0] [0 0 0 1] [1]
[insert#1](x1, x2) = [0 0 0 1] x1 + [0 0 0 0] x2 + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 1 1 0] [0 0 0 0] [0]
[0 0 0 1] [1 0 0 0] [0]
[::](x1, x2) = [0 0 0 0] x1 + [0 0 0 1] x2 + [1]
[0 0 0 0] [0 0 1 0] [1]
[0 0 0 0] [0 1 1 0] [0]
[1 0 1 0] [0 0 0 1] [0 0 0
1] [1 0 1 0] [1]
[insert#2](x1, x2, x3, x4) = [1 1 0 0] x1 + [0 0 0 0] x2 + [0 0 0
0] x3 + [0 1 1 0] x4 + [0]
[1 0 1 0] [0 0 0 0] [0 0 0
0] [0 0 1 0] [1]
[0 1 0 0] [0 0 0 0] [0 0 0
0] [0 0 1 1] [1]
[1]
[nil] = [1]
[0]
[0]
[0]
[#false] = [1]
[1]
[1]
[0]
[#true] = [1]
[1]
[1]
[0 0 0 1] [1 0 1 0] [1]
[insertD](x1, x2) = [0 0 0 0] x1 + [0 0 0 1] x2 + [1]
[0 0 0 0] [0 0 1 0] [1]
[0 0 0 0] [0 1 1 0] [0]
[1 0 1 0] [0 0 0 1] [0]
[insertD#1](x1, x2) = [0 0 0 1] x1 + [0 0 0 0] x2 + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 1 1 0] [0 0 0 0] [0]
[1 0 1 0] [0 0 0 1] [0 0 0
1] [1 0 1 0] [0]
[insertD#2](x1, x2, x3, x4) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0 0 0
0] x3 + [0 1 1 0] x4 + [1]
[0 1 1 0] [0 0 0 0] [0 0 0
0] [0 0 1 0] [0]
[0 1 1 0] [0 0 0 0] [0 0 0
0] [0 0 1 1] [0]
[1 1 0 1] [1]
[insertionsort](x1) = [0 0 0 1] x1 + [1]
[0 0 1 0] [0]
[0 1 1 0] [0]
[1 1 0 1] [1]
[insertionsort#1](x1) = [0 0 0 1] x1 + [1]
[0 0 1 0] [0]
[0 1 1 0] [0]
[1 1 1 1] [1]
[insertionsortD](x1) = [0 0 0 1] x1 + [1]
[0 0 1 0] [1]
[0 1 1 0] [0]
[1 1 1 1] [1]
[insertionsortD#1](x1) = [0 0 0 1] x1 + [1]
[0 0 1 0] [1]
[0 1 1 0] [0]
[0]
[#EQ] = [1]
[1]
[1]
[0]
[#GT] = [1]
[1]
[1]
[0]
[#LT] = [0]
[1]
[1]
This order satisfies following ordering constraints
[#abs(#0())] = [2]
[3]
[2]
[2]
> [0]
[1]
[1]
[0]
= [#0()]
[#abs(#neg(@x))] = [1 1 1 0] [1]
[1 1 2 1] @x + [1]
[1 0 1 0] [1]
[1 1 1 0] [0]
> [1 0 0 0] [0]
[0 1 0 1] @x + [1]
[0 0 1 0] [1]
[0 0 1 0] [0]
= [#pos(@x)]
[#abs(#pos(@x))] = [1 1 0 1] [2]
[1 1 2 1] @x + [3]
[1 0 1 0] [2]
[1 1 1 1] [2]
> [1 0 0 0] [0]
[0 1 0 1] @x + [1]
[0 0 1 0] [1]
[0 0 1 0] [0]
= [#pos(@x)]
[#abs(#s(@x))] = [0 0 1 1] [2]
[1 1 3 1] @x + [2]
[0 0 1 0] [1]
[0 0 2 1] [1]
> [0 0 0 0] [0]
[1 1 2 1] @x + [2]
[0 0 1 0] [1]
[0 0 1 0] [0]
= [#pos(#s(@x))]
[#less(@x, @y)] = [0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] @x + [0 0 0 0] @y + [1]
[0 0 0 0] [0 0 0 0] [1]
[0 1 1 1] [0 1 0 1] [0]
>= [0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] @x + [0 0 0 0] @y + [1]
[0 0 0 0] [0 0 0 0] [1]
[0 1 1 1] [0 1 0 1] [0]
= [#cklt(#compare(@x, @y))]
[#compare(#0(), #0())] = [0]
[2]
[1]
[3]
>= [0]
[1]
[1]
[1]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [0 0 0 0] [0]
[1 1 2 1] @y + [1]
[0 0 0 0] [1]
[0 1 1 1] [2]
>= [0]
[1]
[1]
[1]
= [#GT()]
[#compare(#0(), #pos(@y))] = [0 0 0 0] [0]
[1 1 1 1] @y + [2]
[0 0 0 0] [1]
[0 1 1 1] [3]
>= [0]
[0]
[1]
[1]
= [#LT()]
[#compare(#0(), #s(@y))] = [0 0 0 0] [0]
[1 1 2 1] @y + [2]
[0 0 0 0] [1]
[1 1 2 1] [3]
>= [0]
[0]
[1]
[1]
= [#LT()]
[#compare(#neg(@x), #0())] = [0 0 0 0] [0]
[1 1 2 1] @x + [1]
[0 0 0 0] [1]
[0 1 1 1] [1]
>= [0]
[0]
[1]
[1]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [0 0 0 0] [0 0 0 0] [0]
[1 1 2 1] @x + [1 1 2 1] @y + [0]
[0 0 0 0] [0 0 0 0] [1]
[0 1 1 1] [0 1 1 1] [0]
>= [0 0 0 0] [0 0 0 0] [0]
[1 1 0 1] @x + [1 1 0 1] @y + [0]
[0 0 0 0] [0 0 0 0] [1]
[0 1 0 1] [0 1 1 1] [0]
= [#compare(@y, @x)]
[#compare(#neg(@x), #pos(@y))] = [0 0 0 0] [0 0 0 0] [0]
[1 1 2 1] @x + [1 1 1 1] @y + [1]
[0 0 0 0] [0 0 0 0] [1]
[0 1 1 1] [0 1 1 1] [1]
>= [0]
[0]
[1]
[1]
= [#LT()]
[#compare(#pos(@x), #0())] = [0 0 0 0] [0]
[1 1 1 1] @x + [2]
[0 0 0 0] [1]
[0 1 2 1] [3]
>= [0]
[1]
[1]
[1]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [0 0 0 0] [0 0 0 0] [0]
[1 1 1 1] @x + [1 1 2 1] @y + [1]
[0 0 0 0] [0 0 0 0] [1]
[0 1 2 1] [0 1 1 1] [2]
>= [0]
[1]
[1]
[1]
= [#GT()]
[#compare(#pos(@x), #pos(@y))] = [0 0 0 0] [0 0 0 0] [0]
[1 1 1 1] @x + [1 1 1 1] @y + [2]
[0 0 0 0] [0 0 0 0] [1]
[0 1 2 1] [0 1 1 1] [3]
>= [0 0 0 0] [0 0 0 0] [0]
[1 1 0 1] @x + [1 1 0 1] @y + [0]
[0 0 0 0] [0 0 0 0] [1]
[0 1 1 1] [0 1 0 1] [0]
= [#compare(@x, @y)]
[#compare(#s(@x), #0())] = [0 0 0 0] [0]
[1 1 2 1] @x + [2]
[0 0 0 0] [1]
[1 1 3 1] [2]
>= [0]
[1]
[1]
[1]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [0 0 0 0] [0 0 0 0] [0]
[1 1 2 1] @x + [1 1 2 1] @y + [2]
[0 0 0 0] [0 0 0 0] [1]
[1 1 3 1] [1 1 2 1] [2]
>= [0 0 0 0] [0 0 0 0] [0]
[1 1 0 1] @x + [1 1 0 1] @y + [0]
[0 0 0 0] [0 0 0 0] [1]
[0 1 1 1] [0 1 0 1] [0]
= [#compare(@x, @y)]
[#cklt(#EQ())] = [0]
[1]
[1]
[1]
>= [0]
[1]
[1]
[1]
= [#false()]
[#cklt(#GT())] = [0]
[1]
[1]
[1]
>= [0]
[1]
[1]
[1]
= [#false()]
[#cklt(#LT())] = [0]
[1]
[1]
[1]
>= [0]
[1]
[1]
[1]
= [#true()]
[insert(@x, @l)] = [1 0 1 0] [0 0 0 1] [1]
[0 0 0 1] @l + [0 0 0 0] @x + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 1 1 0] [0 0 0 0] [0]
>= [1 0 1 0] [0 0 0 1] [1]
[0 0 0 1] @l + [0 0 0 0] @x + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 1 1 0] [0 0 0 0] [0]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [0 0 0 1] [0 0 0 1] [1 0 1 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 1 0] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 1] [2]
>= [0 0 0 1] [0 0 0 1] [1 0 1 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 1 0] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 1] [2]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [0 0 0 1] [2]
[0 0 0 0] @x + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
> [0 0 0 1] [1]
[0 0 0 0] @x + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [0 0 0 1] [0 0 0 1] [1 0 1 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 1 0] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 1] [2]
> [0 0 0 1] [0 0 0 1] [1 0 0 0] [0]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 1 0] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 1] [2]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [0 0 0 1] [0 0 0 1] [1 0 1 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 1 0] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 1] [2]
> [0 0 0 1] [0 0 0 1] [1 0 1 0] [1]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 1 0] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 1] [2]
= [::(@y, insert(@x, @ys))]
[insertD(@x, @l)] = [1 0 1 0] [0 0 0 1] [1]
[0 0 0 1] @l + [0 0 0 0] @x + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 1 1 0] [0 0 0 0] [0]
> [1 0 1 0] [0 0 0 1] [0]
[0 0 0 1] @l + [0 0 0 0] @x + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 1 1 0] [0 0 0 0] [0]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [0 0 0 1] [0 0 0 1] [1 0 1 0] [1]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 1 0] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 1] [2]
>= [0 0 0 1] [0 0 0 1] [1 0 1 0] [1]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 1 0] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 1] [2]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [0 0 0 1] [1]
[0 0 0 0] @x + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
>= [0 0 0 1] [1]
[0 0 0 0] @x + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [0 0 0 1] [0 0 0 1] [1 0 1 0] [1]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 1 0] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 1] [2]
> [0 0 0 1] [0 0 0 1] [1 0 0 0] [0]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 1 0] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 1] [2]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [0 0 0 1] [0 0 0 1] [1 0 1 0] [1]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 1 0] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 1] [2]
>= [0 0 0 1] [0 0 0 1] [1 0 1 0] [1]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 1 0] @ys + [1]
[0 0 0 0] [0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 0 0] [0 0 1 1] [2]
= [::(@y, insertD(@x, @ys))]
[insertionsort(@l)] = [1 1 0 1] [1]
[0 0 0 1] @l + [1]
[0 0 1 0] [0]
[0 1 1 0] [0]
>= [1 1 0 1] [1]
[0 0 0 1] @l + [1]
[0 0 1 0] [0]
[0 1 1 0] [0]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [0 0 0 1] [1 1 1 1] [2]
[0 0 0 0] @x + [0 1 1 0] @xs + [1]
[0 0 0 0] [0 0 1 0] [1]
[0 0 0 0] [0 0 1 1] [2]
>= [0 0 0 1] [1 1 1 1] [2]
[0 0 0 0] @x + [0 1 1 0] @xs + [1]
[0 0 0 0] [0 0 1 0] [1]
[0 0 0 0] [0 0 1 1] [1]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [3]
[1]
[0]
[1]
> [1]
[1]
[0]
[0]
= [nil()]
[insertionsortD(@l)] = [1 1 1 1] [1]
[0 0 0 1] @l + [1]
[0 0 1 0] [1]
[0 1 1 0] [0]
>= [1 1 1 1] [1]
[0 0 0 1] @l + [1]
[0 0 1 0] [1]
[0 1 1 0] [0]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [0 0 0 1] [1 1 2 1] [3]
[0 0 0 0] @x + [0 1 1 0] @xs + [1]
[0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 1 1] [2]
>= [0 0 0 1] [1 1 2 1] [3]
[0 0 0 0] @x + [0 1 1 0] @xs + [1]
[0 0 0 0] [0 0 1 0] [2]
[0 0 0 0] [0 0 1 1] [2]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [3]
[1]
[1]
[1]
> [1]
[1]
[0]
[0]
= [nil()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs: { #less(@x, @y) -> #cklt(#compare(@x, @y)) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 4' to
orient following rules strictly.
Trs: { #less(@x, @y) -> #cklt(#compare(@x, @y)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^3)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(#cklt) = {1}, Uargs(insert) = {2}, Uargs(::) = {2},
Uargs(insert#2) = {1}, Uargs(insertD) = {2}, Uargs(insertD#2) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA) and not(IDA(3)).
[0]
[#0] = [0]
[0]
[1]
[1 0 1 0] [0]
[#abs](x1) = [1 1 0 0] x1 + [0]
[1 1 1 1] [0]
[1 1 0 1] [1]
[1 0 0 0] [1]
[#neg](x1) = [0 1 0 0] x1 + [0]
[0 0 1 0] [1]
[0 1 0 1] [1]
[1 0 1 0] [0]
[#pos](x1) = [0 1 0 0] x1 + [0]
[0 1 0 0] [0]
[0 1 0 1] [0]
[1 0 0 0] [0]
[#s](x1) = [0 1 0 0] x1 + [0]
[0 0 1 0] [1]
[0 0 0 1] [1]
[0 0 0 0] [0 0 0 0] [1]
[#less](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [1]
[0 0 1 1] [0 0 0 1] [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
[#compare](x1, x2) = [0 0 0 1] x1 + [0 0 0 1] x2 + [0]
[0 0 0 0] [0 0 0 0] [1]
[0 0 0 1] [0 1 0 1] [1]
[1 0 0 0] [0]
[#cklt](x1) = [0 0 1 0] x1 + [0]
[0 1 0 0] [0]
[0 0 0 0] [0]
[0 0 0 1] [1 1 0 0] [1]
[insert](x1, x2) = [0 0 0 0] x1 + [0 1 0 0] x2 + [1]
[0 0 0 0] [0 0 1 0] [1]
[0 0 0 0] [0 1 0 1] [0]
[1 1 0 0] [0 0 0 1] [1]
[insert#1](x1, x2) = [0 1 0 0] x1 + [0 0 0 0] x2 + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 1 0 1] [0 0 0 0] [0]
[0 0 0 1] [1 0 0 0] [1]
[::](x1, x2) = [0 0 0 0] x1 + [0 1 0 0] x2 + [1]
[0 0 0 0] [0 1 0 0] [0]
[0 0 0 0] [0 0 1 1] [0]
[1 1 0 1] [0 0 0 1] [0 0 0
1] [1 1 0 0] [1]
[insert#2](x1, x2, x3, x4) = [0 1 0 0] x1 + [0 0 0 0] x2 + [0 0 0
0] x3 + [0 1 0 0] x4 + [1]
[0 0 0 0] [0 0 0 0] [0 0 0
0] [0 1 0 0] [1]
[0 0 0 0] [0 0 0 0] [0 0 0
0] [0 1 1 1] [1]
[0]
[nil] = [0]
[0]
[0]
[0]
[#false] = [1]
[1]
[0]
[0]
[#true] = [1]
[0]
[0]
[0 0 0 1] [1 1 0 0] [1]
[insertD](x1, x2) = [0 0 0 0] x1 + [0 1 0 0] x2 + [1]
[0 0 0 0] [0 0 1 0] [1]
[0 0 0 1] [0 1 0 1] [1]
[1 1 0 0] [0 0 0 1] [1]
[insertD#1](x1, x2) = [0 1 0 0] x1 + [0 0 0 0] x2 + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 1 0 1] [0 0 0 1] [1]
[1 1 0 0] [0 0 0 1] [0 0 0
1] [1 1 0 0] [1]
[insertD#2](x1, x2, x3, x4) = [0 1 0 0] x1 + [0 0 0 0] x2 + [0 0 0
0] x3 + [0 1 0 0] x4 + [1]
[0 0 0 0] [0 0 0 0] [0 0 0
0] [0 1 0 0] [1]
[0 1 0 0] [0 0 0 1] [0 0 0
0] [0 1 1 1] [1]
[1 0 1 1] [0]
[insertionsort](x1) = [0 1 0 0] x1 + [0]
[1 0 0 0] [0]
[0 0 1 1] [1]
[1 0 1 1] [0]
[insertionsort#1](x1) = [0 1 0 0] x1 + [0]
[1 0 0 0] [0]
[0 0 1 1] [1]
[1 0 1 1] [0]
[insertionsortD](x1) = [0 1 0 0] x1 + [0]
[1 0 1 1] [0]
[1 0 1 1] [0]
[1 0 1 1] [0]
[insertionsortD#1](x1) = [0 1 0 0] x1 + [0]
[1 0 1 1] [0]
[1 0 1 1] [0]
[0]
[#EQ] = [1]
[1]
[1]
[0]
[#GT] = [1]
[1]
[1]
[0]
[#LT] = [0]
[1]
[1]
This order satisfies following ordering constraints
[#abs(#0())] = [0]
[0]
[1]
[2]
>= [0]
[0]
[0]
[1]
= [#0()]
[#abs(#neg(@x))] = [1 0 1 0] [2]
[1 1 0 0] @x + [1]
[1 2 1 1] [3]
[1 2 0 1] [3]
> [1 0 1 0] [0]
[0 1 0 0] @x + [0]
[0 1 0 0] [0]
[0 1 0 1] [0]
= [#pos(@x)]
[#abs(#pos(@x))] = [1 1 1 0] [0]
[1 1 1 0] @x + [0]
[1 3 1 1] [0]
[1 2 1 1] [1]
>= [1 0 1 0] [0]
[0 1 0 0] @x + [0]
[0 1 0 0] [0]
[0 1 0 1] [0]
= [#pos(@x)]
[#abs(#s(@x))] = [1 0 1 0] [1]
[1 1 0 0] @x + [0]
[1 1 1 1] [2]
[1 1 0 1] [2]
>= [1 0 1 0] [1]
[0 1 0 0] @x + [0]
[0 1 0 0] [0]
[0 1 0 1] [1]
= [#pos(#s(@x))]
[#less(@x, @y)] = [0 0 0 0] [0 0 0 0] [1]
[0 0 0 0] @x + [0 0 0 0] @y + [1]
[0 0 1 1] [0 0 0 1] [0]
[0 0 0 0] [0 0 0 0] [0]
> [0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] @x + [0 0 0 0] @y + [1]
[0 0 0 1] [0 0 0 1] [0]
[0 0 0 0] [0 0 0 0] [0]
= [#cklt(#compare(@x, @y))]
[#compare(#0(), #0())] = [0]
[2]
[1]
[3]
>= [0]
[1]
[1]
[1]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [0 0 0 0] [0]
[0 1 0 1] @y + [2]
[0 0 0 0] [1]
[0 2 0 1] [3]
>= [0]
[1]
[1]
[1]
= [#GT()]
[#compare(#0(), #pos(@y))] = [0 0 0 0] [0]
[0 1 0 1] @y + [1]
[0 0 0 0] [1]
[0 2 0 1] [2]
>= [0]
[0]
[1]
[1]
= [#LT()]
[#compare(#0(), #s(@y))] = [0 0 0 0] [0]
[0 0 0 1] @y + [2]
[0 0 0 0] [1]
[0 1 0 1] [3]
>= [0]
[0]
[1]
[1]
= [#LT()]
[#compare(#neg(@x), #0())] = [0 0 0 0] [0]
[0 1 0 1] @x + [2]
[0 0 0 0] [1]
[0 1 0 1] [3]
>= [0]
[0]
[1]
[1]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [0 0 0 0] [0 0 0 0] [0]
[0 1 0 1] @x + [0 1 0 1] @y + [2]
[0 0 0 0] [0 0 0 0] [1]
[0 1 0 1] [0 2 0 1] [3]
>= [0 0 0 0] [0 0 0 0] [0]
[0 0 0 1] @x + [0 0 0 1] @y + [0]
[0 0 0 0] [0 0 0 0] [1]
[0 1 0 1] [0 0 0 1] [1]
= [#compare(@y, @x)]
[#compare(#neg(@x), #pos(@y))] = [0 0 0 0] [0 0 0 0] [0]
[0 1 0 1] @x + [0 1 0 1] @y + [1]
[0 0 0 0] [0 0 0 0] [1]
[0 1 0 1] [0 2 0 1] [2]
>= [0]
[0]
[1]
[1]
= [#LT()]
[#compare(#pos(@x), #0())] = [0 0 0 0] [0]
[0 1 0 1] @x + [1]
[0 0 0 0] [1]
[0 1 0 1] [2]
>= [0]
[1]
[1]
[1]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [0 0 0 0] [0 0 0 0] [0]
[0 1 0 1] @x + [0 1 0 1] @y + [1]
[0 0 0 0] [0 0 0 0] [1]
[0 1 0 1] [0 2 0 1] [2]
>= [0]
[1]
[1]
[1]
= [#GT()]
[#compare(#pos(@x), #pos(@y))] = [0 0 0 0] [0 0 0 0] [0]
[0 1 0 1] @x + [0 1 0 1] @y + [0]
[0 0 0 0] [0 0 0 0] [1]
[0 1 0 1] [0 2 0 1] [1]
>= [0 0 0 0] [0 0 0 0] [0]
[0 0 0 1] @x + [0 0 0 1] @y + [0]
[0 0 0 0] [0 0 0 0] [1]
[0 0 0 1] [0 1 0 1] [1]
= [#compare(@x, @y)]
[#compare(#s(@x), #0())] = [0 0 0 0] [0]
[0 0 0 1] @x + [2]
[0 0 0 0] [1]
[0 0 0 1] [3]
>= [0]
[1]
[1]
[1]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [0 0 0 0] [0 0 0 0] [0]
[0 0 0 1] @x + [0 0 0 1] @y + [2]
[0 0 0 0] [0 0 0 0] [1]
[0 0 0 1] [0 1 0 1] [3]
>= [0 0 0 0] [0 0 0 0] [0]
[0 0 0 1] @x + [0 0 0 1] @y + [0]
[0 0 0 0] [0 0 0 0] [1]
[0 0 0 1] [0 1 0 1] [1]
= [#compare(@x, @y)]
[#cklt(#EQ())] = [0]
[1]
[1]
[0]
>= [0]
[1]
[1]
[0]
= [#false()]
[#cklt(#GT())] = [0]
[1]
[1]
[0]
>= [0]
[1]
[1]
[0]
= [#false()]
[#cklt(#LT())] = [0]
[1]
[0]
[0]
>= [0]
[1]
[0]
[0]
= [#true()]
[insert(@x, @l)] = [1 1 0 0] [0 0 0 1] [1]
[0 1 0 0] @l + [0 0 0 0] @x + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 1 0 1] [0 0 0 0] [0]
>= [1 1 0 0] [0 0 0 1] [1]
[0 1 0 0] @l + [0 0 0 0] @x + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 1 0 1] [0 0 0 0] [0]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [0 0 0 1] [0 0 0 1] [1 1 0 0] [3]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[0 0 0 0] [0 0 0 0] [0 1 1 1] [1]
>= [0 0 0 1] [0 0 0 1] [1 1 0 0] [3]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[0 0 0 0] [0 0 0 0] [0 1 1 1] [1]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [0 0 0 1] [1]
[0 0 0 0] @x + [1]
[0 0 0 0] [1]
[0 0 0 0] [0]
>= [0 0 0 1] [1]
[0 0 0 0] @x + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [0 0 0 1] [0 0 0 1] [1 1 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[0 0 0 0] [0 0 0 0] [0 1 1 1] [1]
>= [0 0 0 1] [0 0 0 1] [1 0 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[0 0 0 0] [0 0 0 0] [0 1 1 1] [0]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [0 0 0 1] [0 0 0 1] [1 1 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[0 0 0 0] [0 0 0 0] [0 1 1 1] [1]
>= [0 0 0 1] [0 0 0 1] [1 1 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[0 0 0 0] [0 0 0 0] [0 1 1 1] [1]
= [::(@y, insert(@x, @ys))]
[insertD(@x, @l)] = [1 1 0 0] [0 0 0 1] [1]
[0 1 0 0] @l + [0 0 0 0] @x + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 1 0 1] [0 0 0 1] [1]
>= [1 1 0 0] [0 0 0 1] [1]
[0 1 0 0] @l + [0 0 0 0] @x + [1]
[0 0 1 0] [0 0 0 0] [1]
[0 1 0 1] [0 0 0 1] [1]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [0 0 0 1] [0 0 0 1] [1 1 0 0] [3]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[0 0 0 1] [0 0 0 0] [0 1 1 1] [2]
>= [0 0 0 1] [0 0 0 1] [1 1 0 0] [3]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[0 0 0 1] [0 0 0 0] [0 1 1 1] [2]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [0 0 0 1] [1]
[0 0 0 0] @x + [1]
[0 0 0 0] [1]
[0 0 0 1] [1]
>= [0 0 0 1] [1]
[0 0 0 0] @x + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [0 0 0 1] [0 0 0 1] [1 1 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[0 0 0 1] [0 0 0 0] [0 1 1 1] [2]
>= [0 0 0 1] [0 0 0 1] [1 0 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[0 0 0 0] [0 0 0 0] [0 1 1 1] [0]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [0 0 0 1] [0 0 0 1] [1 1 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[0 0 0 1] [0 0 0 0] [0 1 1 1] [2]
>= [0 0 0 1] [0 0 0 1] [1 1 0 0] [2]
[0 0 0 0] @x + [0 0 0 0] @y + [0 1 0 0] @ys + [2]
[0 0 0 0] [0 0 0 0] [0 1 0 0] [1]
[0 0 0 1] [0 0 0 0] [0 1 1 1] [2]
= [::(@y, insertD(@x, @ys))]
[insertionsort(@l)] = [1 0 1 1] [0]
[0 1 0 0] @l + [0]
[1 0 0 0] [0]
[0 0 1 1] [1]
>= [1 0 1 1] [0]
[0 1 0 0] @l + [0]
[1 0 0 0] [0]
[0 0 1 1] [1]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [0 0 0 1] [1 1 1 1] [1]
[0 0 0 0] @x + [0 1 0 0] @xs + [1]
[0 0 0 1] [1 0 0 0] [1]
[0 0 0 0] [0 1 1 1] [1]
>= [0 0 0 1] [1 1 1 1] [1]
[0 0 0 0] @x + [0 1 0 0] @xs + [1]
[0 0 0 0] [1 0 0 0] [1]
[0 0 0 0] [0 1 1 1] [1]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [0]
[0]
[0]
[1]
>= [0]
[0]
[0]
[0]
= [nil()]
[insertionsortD(@l)] = [1 0 1 1] [0]
[0 1 0 0] @l + [0]
[1 0 1 1] [0]
[1 0 1 1] [0]
>= [1 0 1 1] [0]
[0 1 0 0] @l + [0]
[1 0 1 1] [0]
[1 0 1 1] [0]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [0 0 0 1] [1 1 1 1] [1]
[0 0 0 0] @x + [0 1 0 0] @xs + [1]
[0 0 0 1] [1 1 1 1] [1]
[0 0 0 1] [1 1 1 1] [1]
>= [0 0 0 1] [1 1 1 1] [1]
[0 0 0 0] @x + [0 1 0 0] @xs + [1]
[0 0 0 0] [1 0 1 1] [1]
[0 0 0 1] [1 1 1 1] [1]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [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:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, #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)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^3))