tct
YES(O(1),O(n^1))
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ group3(@l) -> group3#1(@l)
, group3#1(::(@x, @xs)) -> group3#2(@xs, @x)
, group3#1(nil()) -> nil()
, group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)
, group3#2(nil(), @x) -> nil()
, group3#3(::(@z, @zs), @x, @y) ->
::(tuple#3(@x, @y, @z), group3(@zs))
, group3#3(nil(), @x, @y) -> nil()
, zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
, zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)
, zip3#1(nil(), @l2, @l3) -> nil()
, zip3#2(::(@y, @ys), @l3, @x, @xs) ->
zip3#3(@l3, @x, @xs, @y, @ys)
, zip3#2(nil(), @l3, @x, @xs) -> nil()
, zip3#3(::(@z, @zs), @x, @xs, @y, @ys) ->
::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
, zip3#3(nil(), @x, @xs, @y, @ys) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We add following dependency pairs
Strict DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#2^#(nil(), @x) -> c_5()
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, group3#3^#(nil(), @x, @y) -> c_7()
, zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#1^#(nil(), @l2, @l3) -> c_10()
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
, zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() }
and replace the set of basic marked basic terms accordingly.
We apply the transformation 'usablerules' on the sub-problem:
Strict DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#2^#(nil(), @x) -> c_5()
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, group3#3^#(nil(), @x, @y) -> c_7()
, zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#1^#(nil(), @l2, @l3) -> c_10()
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
, zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() }
Strict Trs:
{ group3(@l) -> group3#1(@l)
, group3#1(::(@x, @xs)) -> group3#2(@xs, @x)
, group3#1(nil()) -> nil()
, group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)
, group3#2(nil(), @x) -> nil()
, group3#3(::(@z, @zs), @x, @y) ->
::(tuple#3(@x, @y, @z), group3(@zs))
, group3#3(nil(), @x, @y) -> nil()
, zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
, zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)
, zip3#1(nil(), @l2, @l3) -> nil()
, zip3#2(::(@y, @ys), @l3, @x, @xs) ->
zip3#3(@l3, @x, @xs, @y, @ys)
, zip3#2(nil(), @l3, @x, @xs) -> nil()
, zip3#3(::(@z, @zs), @x, @xs, @y, @ys) ->
::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
, zip3#3(nil(), @x, @xs, @y, @ys) -> nil() }
StartTerms: basic terms
Strategy: innermost
No rule is usable.
We apply the transformation 'compose (addition)' on the
sub-problem:
Strict DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#2^#(nil(), @x) -> c_5()
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, group3#3^#(nil(), @x, @y) -> c_7()
, zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#1^#(nil(), @l2, @l3) -> c_10()
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
, zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() }
StartTerms: basic terms
Strategy: innermost
We use the processor 'weightgap of dimension 2, maximal degree 1,
cbits 3' to orient following rules strictly.
DPs: { group3^#(@l) -> group3#1^#(@l) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)). These rulesare moved into the corresponding weak
component(s).
Sub-proof:
----------
The weightgap principle applies (using the following constant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(::) = {}, Uargs(tuple#3) = {}, Uargs(group3^#) = {},
Uargs(group3#1^#) = {}, Uargs(group3#2^#) = {},
Uargs(group3#3^#) = {}, Uargs(zip3^#) = {}, Uargs(zip3#1^#) = {},
Uargs(zip3#2^#) = {}, Uargs(zip3#3^#) = {}
TcT has computed following constructor-restricted matrix
interpretation. Note that the diagonal of the component-wise maxima
of interpretation-entries (of constructors) contains no more than 1
non-zero entries.
[::](x1, x2) = [1 0] x2 + [0]
[0 0] [0]
[nil] = [0]
[0]
[tuple#3](x1, x2, x3) = [0]
[0]
[group3^#](x1) = [2]
[0]
[group3#1^#](x1) = [0]
[0]
[group3#2^#](x1, x2) = [0]
[0]
[c_3] = [0]
[0]
[group3#3^#](x1, x2, x3) = [0]
[0]
[c_5] = [0]
[0]
[c_7] = [0]
[0]
[zip3^#](x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0]
[0 2] [2 2] [0]
[zip3#1^#](x1, x2, x3) = [0 0] x2 + [0]
[2 2] [0]
[zip3#2^#](x1, x2, x3, x4) = [0 0] x2 + [0 0] x4 + [0]
[2 2] [2 2] [0]
[c_10] = [0]
[0]
[zip3#3^#](x1, x2, x3, x4, x5) = [0 0] x3 + [0 0] x5 + [0]
[2 2] [2 2] [0]
[c_12] = [0]
[0]
[c_14] = [0]
[0]
This order satisfies following ordering constraints
[group3^#(@l)] = [2]
[0]
> [0]
[0]
= [group3#1^#(@l)]
[group3#1^#(::(@x, @xs))] = [0]
[0]
>= [0]
[0]
= [group3#2^#(@xs, @x)]
[group3#1^#(nil())] = [0]
[0]
>= [0]
[0]
= [c_3()]
[group3#2^#(::(@y, @ys), @x)] = [0]
[0]
>= [0]
[0]
= [group3#3^#(@ys, @x, @y)]
[group3#2^#(nil(), @x)] = [0]
[0]
>= [0]
[0]
= [c_5()]
[group3#3^#(::(@z, @zs), @x, @y)] = [0]
[0]
? [2]
[0]
= [group3^#(@zs)]
[group3#3^#(nil(), @x, @y)] = [0]
[0]
>= [0]
[0]
= [c_7()]
[zip3^#(@l1, @l2, @l3)] = [0 0] @l1 + [0 0] @l2 + [0]
[0 2] [2 2] [0]
>= [0 0] @l2 + [0]
[2 2] [0]
= [zip3#1^#(@l1, @l2, @l3)]
[zip3#1^#(::(@x, @xs), @l2, @l3)] = [0 0] @l2 + [0]
[2 2] [0]
? [0 0] @l3 + [0 0] @xs + [0]
[2 2] [2 2] [0]
= [zip3#2^#(@l2, @l3, @x, @xs)]
[zip3#1^#(nil(), @l2, @l3)] = [0 0] @l2 + [0]
[2 2] [0]
>= [0]
[0]
= [c_10()]
[zip3#2^#(::(@y, @ys), @l3, @x, @xs)] = [0 0] @l3 + [0 0] @xs + [0]
[2 2] [2 2] [0]
? [0 0] @xs + [0 0] @ys + [0]
[2 2] [2 2] [0]
= [zip3#3^#(@l3, @x, @xs, @y, @ys)]
[zip3#2^#(nil(), @l3, @x, @xs)] = [0 0] @l3 + [0 0] @xs + [0]
[2 2] [2 2] [0]
>= [0]
[0]
= [c_12()]
[zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys)] = [0 0] @xs + [0 0] @ys + [0]
[2 2] [2 2] [0]
>= [0 0] @xs + [0 0] @ys + [0]
[0 2] [2 2] [0]
= [zip3^#(@xs, @ys, @zs)]
[zip3#3^#(nil(), @x, @xs, @y, @ys)] = [0 0] @xs + [0 0] @ys + [0]
[2 2] [2 2] [0]
>= [0]
[0]
= [c_14()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict DPs:
{ group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#2^#(nil(), @x) -> c_5()
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, group3#3^#(nil(), @x, @y) -> c_7()
, zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#1^#(nil(), @l2, @l3) -> c_10()
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
, zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() }
Weak DPs: { group3^#(@l) -> group3#1^#(@l) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
We consider the (estimated) dependency graph
1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
-->_1 group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y) :3
-->_1 group3#2^#(nil(), @x) -> c_5() :4
2: group3#1^#(nil()) -> c_3()
3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
-->_1 group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) :5
-->_1 group3#3^#(nil(), @x, @y) -> c_7() :6
4: group3#2^#(nil(), @x) -> c_5()
5: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
-->_1 group3^#(@l) -> group3#1^#(@l) :14
6: group3#3^#(nil(), @x, @y) -> c_7()
7: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
-->_1 zip3#1^#(::(@x, @xs), @l2, @l3) ->
zip3#2^#(@l2, @l3, @x, @xs) :8
-->_1 zip3#1^#(nil(), @l2, @l3) -> c_10() :9
8: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
-->_1 zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys) :10
-->_1 zip3#2^#(nil(), @l3, @x, @xs) -> c_12() :11
9: zip3#1^#(nil(), @l2, @l3) -> c_10()
10: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
-->_1 zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) :12
-->_1 zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() :13
11: zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
12: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs)
-->_1 zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3) :7
13: zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14()
14: group3^#(@l) -> group3#1^#(@l)
-->_1 group3#1^#(nil()) -> c_3() :2
-->_1 group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {9} and add Pre({9}) = {7} to the strict component.
- We remove {11} and add Pre({11}) = {8} to the strict component.
- We remove {13} and add Pre({13}) = {10} to the strict component.
- We remove {4} and add Pre({4}) = {1} to the strict component.
- We remove {6} and add Pre({6}) = {3} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict DPs:
{ group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Weak DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#2^#(nil(), @x) -> c_5()
, group3#3^#(nil(), @x, @y) -> c_7()
, zip3#1^#(nil(), @l2, @l3) -> c_10()
, zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
, zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
We consider the the dependency graph
->5:{1,9,4,3}
|
|->8:{2}
|
|->6:{10} Weak SCC
|
`->7:{11} Weak SCC
->1:{5,8,7,6}
|
|->2:{12} Weak SCC
|
|->3:{13} Weak SCC
|
`->4:{14} Weak SCC
Here dependency-pairs are as follows:
Strict DPs:
{ 1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, 2: group3#1^#(nil()) -> c_3()
, 3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, 4: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, 5: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, 6: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, 7: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, 8: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Weak DPs:
{ 9: group3^#(@l) -> group3#1^#(@l)
, 10: group3#2^#(nil(), @x) -> c_5()
, 11: group3#3^#(nil(), @x, @y) -> c_7()
, 12: zip3#1^#(nil(), @l2, @l3) -> c_10()
, 13: zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
, 14: zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 12: zip3#1^#(nil(), @l2, @l3) -> c_10()
, 13: zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
, 14: zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14()
, 10: group3#2^#(nil(), @x) -> c_5()
, 11: group3#3^#(nil(), @x, @y) -> c_7() }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict DPs:
{ group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Weak DPs: { group3^#(@l) -> group3#1^#(@l) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
We employ 'linear path analysis' using the following approximated
dependency graph:
->2:{1,9,4,3} [ ? ]
|
`->3:{2} [ YES(O(1),O(n^1)) ]
->1:{5,8,7,6} [ YES(O(1),O(n^1)) ]
Here dependency-pairs are as follows:
Strict DPs:
{ 1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, 2: group3#1^#(nil()) -> c_3()
, 3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, 4: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, 5: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, 6: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, 7: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, 8: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Weak DPs:
{ 9: group3^#(@l) -> group3#1^#(@l) }
* Path 2:{1,9,4,3}->3:{2}: YES(O(1),O(n^1))
-----------------------------------------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
Weak DPs: { group3^#(@l) -> group3#1^#(@l) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We consider the (estimated) dependency graph
1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
-->_1 group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y) :3
2: group3#1^#(nil()) -> c_3()
3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
-->_1 group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) :4
4: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
-->_1 group3^#(@l) -> group3#1^#(@l) :5
5: group3^#(@l) -> group3#1^#(@l)
-->_1 group3#1^#(nil()) -> c_3() :2
-->_1 group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {4} and add Pre({4}) = {3} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y) }
Weak DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We consider the (estimated) dependency graph
1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
-->_1 group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y) :3
2: group3#1^#(nil()) -> c_3()
3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
-->_1 group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) :5
4: group3^#(@l) -> group3#1^#(@l)
-->_1 group3#1^#(nil()) -> c_3() :2
-->_1 group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) :1
5: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
-->_1 group3^#(@l) -> group3#1^#(@l) :4
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {1} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3() }
Weak DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 2: group3#1^#(nil()) -> c_3() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(::) = {}, Uargs(tuple#3) = {}, Uargs(group3^#) = {},
Uargs(group3#1^#) = {}, Uargs(group3#2^#) = {},
Uargs(group3#3^#) = {}, Uargs(zip3^#) = {}, Uargs(zip3#1^#) = {},
Uargs(zip3#2^#) = {}, Uargs(zip3#3^#) = {}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[::](x1, x2) = [1] x2 + [0]
[nil] = [3]
[tuple#3](x1, x2, x3) = [0]
[group3^#](x1) = [2] x1 + [0]
[group3#1^#](x1) = [2] x1 + [0]
[group3#2^#](x1, x2) = [2] x1 + [0]
[c_3] = [1]
[group3#3^#](x1, x2, x3) = [2] x1 + [0]
[zip3^#](x1, x2, x3) = [0]
[zip3#1^#](x1, x2, x3) = [0]
[zip3#2^#](x1, x2, x3, x4) = [0]
[zip3#3^#](x1, x2, x3, x4, x5) = [0]
This order satisfies following ordering constraints
[group3^#(@l)] = [2] @l + [0]
>= [2] @l + [0]
= [group3#1^#(@l)]
[group3#1^#(::(@x, @xs))] = [2] @xs + [0]
>= [2] @xs + [0]
= [group3#2^#(@xs, @x)]
[group3#1^#(nil())] = [6]
> [1]
= [c_3()]
[group3#2^#(::(@y, @ys), @x)] = [2] @ys + [0]
>= [2] @ys + [0]
= [group3#3^#(@ys, @x, @y)]
[group3#3^#(::(@z, @zs), @x, @y)] = [2] @zs + [0]
>= [2] @zs + [0]
= [group3^#(@zs)]
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of rules {2}.
Here rules are labeled according to the (estimated) dependency
graph
1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
-->_1 group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y) :4
2: group3#1^#(nil()) -> c_3()
3: group3^#(@l) -> group3#1^#(@l)
-->_1 group3#1^#(nil()) -> c_3() :2
-->_1 group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) :1
4: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
-->_1 group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) :5
5: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
-->_1 group3^#(@l) -> group3#1^#(@l) :3
Overall, we obtain that the number of applications of rules {2} is
given by YES(?,O(n^1)).
We apply the transformation 'removetails' on the sub-problem:
Strict DPs: { group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) }
Weak DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{1,2,5,4}
|
`->2:{3} Weak SCC
Here dependency-pairs are as follows:
Strict DPs:
{ 1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) }
Weak DPs:
{ 2: group3^#(@l) -> group3#1^#(@l)
, 3: group3#1^#(nil()) -> c_3()
, 4: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, 5: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 3: group3#1^#(nil()) -> c_3() }
We apply the transformation 'simpKP' on the sub-problem:
Strict DPs: { group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) }
Weak DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
StartTerms: basic terms
Strategy: innermost
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, 2: group3^#(@l) -> group3#1^#(@l)
, 3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, 4: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(::) = {}, Uargs(tuple#3) = {}, Uargs(group3^#) = {},
Uargs(group3#1^#) = {}, Uargs(group3#2^#) = {},
Uargs(group3#3^#) = {}, Uargs(zip3^#) = {}, Uargs(zip3#1^#) = {},
Uargs(zip3#2^#) = {}, Uargs(zip3#3^#) = {}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[::](x1, x2) = [1] x2 + [2]
[nil] = [0]
[tuple#3](x1, x2, x3) = [0]
[group3^#](x1) = [2] x1 + [3]
[group3#1^#](x1) = [2] x1 + [0]
[group3#2^#](x1, x2) = [2] x1 + [0]
[c_3] = [0]
[group3#3^#](x1, x2, x3) = [2] x1 + [3]
[zip3^#](x1, x2, x3) = [0]
[zip3#1^#](x1, x2, x3) = [0]
[zip3#2^#](x1, x2, x3, x4) = [0]
[zip3#3^#](x1, x2, x3, x4, x5) = [0]
This order satisfies following ordering constraints
[group3^#(@l)] = [2] @l + [3]
> [2] @l + [0]
= [group3#1^#(@l)]
[group3#1^#(::(@x, @xs))] = [2] @xs + [4]
> [2] @xs + [0]
= [group3#2^#(@xs, @x)]
[group3#2^#(::(@y, @ys), @x)] = [2] @ys + [4]
> [2] @ys + [3]
= [group3#3^#(@ys, @x, @y)]
[group3#3^#(::(@z, @zs), @x, @y)] = [2] @zs + [7]
> [2] @zs + [3]
= [group3^#(@zs)]
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of rules
{1,2,3,4}. Here rules are labeled according to the (estimated)
dependency graph
1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
-->_1 group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y) :3
2: group3^#(@l) -> group3#1^#(@l)
-->_1 group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) :1
3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
-->_1 group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) :4
4: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
-->_1 group3^#(@l) -> group3#1^#(@l) :2
Overall, we obtain that the number of applications of rules
{1,2,3,4} is given by YES(?,O(n^1)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{1,4,3,2} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: group3^#(@l) -> group3#1^#(@l)
, 2: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, 3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, 4: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 1: group3^#(@l) -> group3#1^#(@l)
, 4: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, 3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, 2: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) }
We apply the transformation 'usablerules' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We apply the transformation 'trivial' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We consider the dependency graph
empty
All SCCs are trivial and dependency pairs can be removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
* Path 1:{5,8,7,6}: YES(O(1),O(n^1))
----------------------------------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We consider the (estimated) dependency graph
1: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
-->_1 zip3#1^#(::(@x, @xs), @l2, @l3) ->
zip3#2^#(@l2, @l3, @x, @xs) :2
2: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
-->_1 zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys) :3
3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
-->_1 zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) :4
4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
-->_1 zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {4} and add Pre({4}) = {3} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys) }
Weak DPs:
{ zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We consider the (estimated) dependency graph
1: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
-->_1 zip3#1^#(::(@x, @xs), @l2, @l3) ->
zip3#2^#(@l2, @l3, @x, @xs) :2
2: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
-->_1 zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys) :3
3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
-->_1 zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) :4
4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
-->_1 zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {2} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs) }
Weak DPs:
{ zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We consider the (estimated) dependency graph
1: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
-->_1 zip3#1^#(::(@x, @xs), @l2, @l3) ->
zip3#2^#(@l2, @l3, @x, @xs) :2
2: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
-->_1 zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys) :3
3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
-->_1 zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) :4
4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
-->_1 zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {2} and add Pre({2}) = {1} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3) }
Weak DPs:
{ zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, 3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, 4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(::) = {}, Uargs(tuple#3) = {}, Uargs(group3^#) = {},
Uargs(group3#1^#) = {}, Uargs(group3#2^#) = {},
Uargs(group3#3^#) = {}, Uargs(zip3^#) = {}, Uargs(zip3#1^#) = {},
Uargs(zip3#2^#) = {}, Uargs(zip3#3^#) = {}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[::](x1, x2) = [1] x2 + [2]
[nil] = [0]
[tuple#3](x1, x2, x3) = [0]
[group3^#](x1) = [0]
[group3#1^#](x1) = [0]
[group3#2^#](x1, x2) = [0]
[group3#3^#](x1, x2, x3) = [0]
[zip3^#](x1, x2, x3) = [2] x2 + [2]
[zip3#1^#](x1, x2, x3) = [2] x2 + [0]
[zip3#2^#](x1, x2, x3, x4) = [2] x1 + [0]
[zip3#3^#](x1, x2, x3, x4, x5) = [2] x5 + [3]
This order satisfies following ordering constraints
[zip3^#(@l1, @l2, @l3)] = [2] @l2 + [2]
> [2] @l2 + [0]
= [zip3#1^#(@l1, @l2, @l3)]
[zip3#1^#(::(@x, @xs), @l2, @l3)] = [2] @l2 + [0]
>= [2] @l2 + [0]
= [zip3#2^#(@l2, @l3, @x, @xs)]
[zip3#2^#(::(@y, @ys), @l3, @x, @xs)] = [2] @ys + [4]
> [2] @ys + [3]
= [zip3#3^#(@l3, @x, @xs, @y, @ys)]
[zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys)] = [2] @ys + [3]
> [2] @ys + [2]
= [zip3^#(@xs, @ys, @zs)]
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of rules
{1,3,4}. Here rules are labeled according to the (estimated)
dependency graph
1: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
-->_1 zip3#1^#(::(@x, @xs), @l2, @l3) ->
zip3#2^#(@l2, @l3, @x, @xs) :2
2: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
-->_1 zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys) :3
3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
-->_1 zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) :4
4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
-->_1 zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3) :1
- The rules {1,3,4} have known complexity. These cover all
predecessors of {2}, their complexity is equally bounded.
Overall, we obtain that the number of applications of rules
{1,2,3,4} is given by YES(?,O(n^1)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{1,4,3,2} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, 2: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, 3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, 4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 1: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, 4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs)
, 3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, 2: zip3#1^#(::(@x, @xs), @l2, @l3) ->
zip3#2^#(@l2, @l3, @x, @xs) }
We apply the transformation 'usablerules' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We apply the transformation 'trivial' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We consider the dependency graph
empty
All SCCs are trivial and dependency pairs can be removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^1))
tct-popstar
YES(O(1),O(n^1))
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ group3(@l) -> group3#1(@l)
, group3#1(::(@x, @xs)) -> group3#2(@xs, @x)
, group3#1(nil()) -> nil()
, group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)
, group3#2(nil(), @x) -> nil()
, group3#3(::(@z, @zs), @x, @y) ->
::(tuple#3(@x, @y, @z), group3(@zs))
, group3#3(nil(), @x, @y) -> nil()
, zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
, zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)
, zip3#1(nil(), @l2, @l3) -> nil()
, zip3#2(::(@y, @ys), @l3, @x, @xs) ->
zip3#3(@l3, @x, @xs, @y, @ys)
, zip3#2(nil(), @l3, @x, @xs) -> nil()
, zip3#3(::(@z, @zs), @x, @xs, @y, @ys) ->
::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
, zip3#3(nil(), @x, @xs, @y, @ys) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We add following dependency pairs
Strict DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#2^#(nil(), @x) -> c_5()
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, group3#3^#(nil(), @x, @y) -> c_7()
, zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#1^#(nil(), @l2, @l3) -> c_10()
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
, zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() }
and replace the set of basic marked basic terms accordingly.
We apply the transformation 'usablerules' on the sub-problem:
Strict DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#2^#(nil(), @x) -> c_5()
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, group3#3^#(nil(), @x, @y) -> c_7()
, zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#1^#(nil(), @l2, @l3) -> c_10()
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
, zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() }
Strict Trs:
{ group3(@l) -> group3#1(@l)
, group3#1(::(@x, @xs)) -> group3#2(@xs, @x)
, group3#1(nil()) -> nil()
, group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y)
, group3#2(nil(), @x) -> nil()
, group3#3(::(@z, @zs), @x, @y) ->
::(tuple#3(@x, @y, @z), group3(@zs))
, group3#3(nil(), @x, @y) -> nil()
, zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3)
, zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs)
, zip3#1(nil(), @l2, @l3) -> nil()
, zip3#2(::(@y, @ys), @l3, @x, @xs) ->
zip3#3(@l3, @x, @xs, @y, @ys)
, zip3#2(nil(), @l3, @x, @xs) -> nil()
, zip3#3(::(@z, @zs), @x, @xs, @y, @ys) ->
::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
, zip3#3(nil(), @x, @xs, @y, @ys) -> nil() }
StartTerms: basic terms
Strategy: innermost
No rule is usable.
We apply the transformation 'compose (addition)' on the
sub-problem:
Strict DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#2^#(nil(), @x) -> c_5()
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, group3#3^#(nil(), @x, @y) -> c_7()
, zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#1^#(nil(), @l2, @l3) -> c_10()
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
, zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() }
StartTerms: basic terms
Strategy: innermost
We use the processor 'weightgap of dimension 2, maximal degree 1,
cbits 3' to orient following rules strictly.
DPs: { group3^#(@l) -> group3#1^#(@l) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)). These rulesare moved into the corresponding weak
component(s).
Sub-proof:
----------
The weightgap principle applies (using the following constant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(::) = {}, Uargs(tuple#3) = {}, Uargs(group3^#) = {},
Uargs(group3#1^#) = {}, Uargs(group3#2^#) = {},
Uargs(group3#3^#) = {}, Uargs(zip3^#) = {}, Uargs(zip3#1^#) = {},
Uargs(zip3#2^#) = {}, Uargs(zip3#3^#) = {}
TcT has computed following constructor-restricted matrix
interpretation. Note that the diagonal of the component-wise maxima
of interpretation-entries (of constructors) contains no more than 1
non-zero entries.
[::](x1, x2) = [1 0] x2 + [0]
[0 0] [0]
[nil] = [0]
[0]
[tuple#3](x1, x2, x3) = [0]
[0]
[group3^#](x1) = [2]
[0]
[group3#1^#](x1) = [0]
[0]
[group3#2^#](x1, x2) = [0]
[0]
[c_3] = [0]
[0]
[group3#3^#](x1, x2, x3) = [0]
[0]
[c_5] = [0]
[0]
[c_7] = [0]
[0]
[zip3^#](x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0]
[0 2] [2 2] [0]
[zip3#1^#](x1, x2, x3) = [0 0] x2 + [0]
[2 2] [0]
[zip3#2^#](x1, x2, x3, x4) = [0 0] x2 + [0 0] x4 + [0]
[2 2] [2 2] [0]
[c_10] = [0]
[0]
[zip3#3^#](x1, x2, x3, x4, x5) = [0 0] x3 + [0 0] x5 + [0]
[2 2] [2 2] [0]
[c_12] = [0]
[0]
[c_14] = [0]
[0]
This order satisfies following ordering constraints
[group3^#(@l)] = [2]
[0]
> [0]
[0]
= [group3#1^#(@l)]
[group3#1^#(::(@x, @xs))] = [0]
[0]
>= [0]
[0]
= [group3#2^#(@xs, @x)]
[group3#1^#(nil())] = [0]
[0]
>= [0]
[0]
= [c_3()]
[group3#2^#(::(@y, @ys), @x)] = [0]
[0]
>= [0]
[0]
= [group3#3^#(@ys, @x, @y)]
[group3#2^#(nil(), @x)] = [0]
[0]
>= [0]
[0]
= [c_5()]
[group3#3^#(::(@z, @zs), @x, @y)] = [0]
[0]
? [2]
[0]
= [group3^#(@zs)]
[group3#3^#(nil(), @x, @y)] = [0]
[0]
>= [0]
[0]
= [c_7()]
[zip3^#(@l1, @l2, @l3)] = [0 0] @l1 + [0 0] @l2 + [0]
[0 2] [2 2] [0]
>= [0 0] @l2 + [0]
[2 2] [0]
= [zip3#1^#(@l1, @l2, @l3)]
[zip3#1^#(::(@x, @xs), @l2, @l3)] = [0 0] @l2 + [0]
[2 2] [0]
? [0 0] @l3 + [0 0] @xs + [0]
[2 2] [2 2] [0]
= [zip3#2^#(@l2, @l3, @x, @xs)]
[zip3#1^#(nil(), @l2, @l3)] = [0 0] @l2 + [0]
[2 2] [0]
>= [0]
[0]
= [c_10()]
[zip3#2^#(::(@y, @ys), @l3, @x, @xs)] = [0 0] @l3 + [0 0] @xs + [0]
[2 2] [2 2] [0]
? [0 0] @xs + [0 0] @ys + [0]
[2 2] [2 2] [0]
= [zip3#3^#(@l3, @x, @xs, @y, @ys)]
[zip3#2^#(nil(), @l3, @x, @xs)] = [0 0] @l3 + [0 0] @xs + [0]
[2 2] [2 2] [0]
>= [0]
[0]
= [c_12()]
[zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys)] = [0 0] @xs + [0 0] @ys + [0]
[2 2] [2 2] [0]
>= [0 0] @xs + [0 0] @ys + [0]
[0 2] [2 2] [0]
= [zip3^#(@xs, @ys, @zs)]
[zip3#3^#(nil(), @x, @xs, @y, @ys)] = [0 0] @xs + [0 0] @ys + [0]
[2 2] [2 2] [0]
>= [0]
[0]
= [c_14()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict DPs:
{ group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#2^#(nil(), @x) -> c_5()
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, group3#3^#(nil(), @x, @y) -> c_7()
, zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#1^#(nil(), @l2, @l3) -> c_10()
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
, zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() }
Weak DPs: { group3^#(@l) -> group3#1^#(@l) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
We consider the (estimated) dependency graph
1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
-->_1 group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y) :3
-->_1 group3#2^#(nil(), @x) -> c_5() :4
2: group3#1^#(nil()) -> c_3()
3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
-->_1 group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) :5
-->_1 group3#3^#(nil(), @x, @y) -> c_7() :6
4: group3#2^#(nil(), @x) -> c_5()
5: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
-->_1 group3^#(@l) -> group3#1^#(@l) :14
6: group3#3^#(nil(), @x, @y) -> c_7()
7: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
-->_1 zip3#1^#(::(@x, @xs), @l2, @l3) ->
zip3#2^#(@l2, @l3, @x, @xs) :8
-->_1 zip3#1^#(nil(), @l2, @l3) -> c_10() :9
8: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
-->_1 zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys) :10
-->_1 zip3#2^#(nil(), @l3, @x, @xs) -> c_12() :11
9: zip3#1^#(nil(), @l2, @l3) -> c_10()
10: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
-->_1 zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) :12
-->_1 zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() :13
11: zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
12: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs)
-->_1 zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3) :7
13: zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14()
14: group3^#(@l) -> group3#1^#(@l)
-->_1 group3#1^#(nil()) -> c_3() :2
-->_1 group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {9} and add Pre({9}) = {7} to the strict component.
- We remove {11} and add Pre({11}) = {8} to the strict component.
- We remove {13} and add Pre({13}) = {10} to the strict component.
- We remove {4} and add Pre({4}) = {1} to the strict component.
- We remove {6} and add Pre({6}) = {3} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict DPs:
{ group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Weak DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#2^#(nil(), @x) -> c_5()
, group3#3^#(nil(), @x, @y) -> c_7()
, zip3#1^#(nil(), @l2, @l3) -> c_10()
, zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
, zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
We consider the the dependency graph
->5:{1,9,4,3}
|
|->8:{2}
|
|->6:{10} Weak SCC
|
`->7:{11} Weak SCC
->1:{5,8,7,6}
|
|->2:{12} Weak SCC
|
|->3:{13} Weak SCC
|
`->4:{14} Weak SCC
Here dependency-pairs are as follows:
Strict DPs:
{ 1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, 2: group3#1^#(nil()) -> c_3()
, 3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, 4: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, 5: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, 6: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, 7: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, 8: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Weak DPs:
{ 9: group3^#(@l) -> group3#1^#(@l)
, 10: group3#2^#(nil(), @x) -> c_5()
, 11: group3#3^#(nil(), @x, @y) -> c_7()
, 12: zip3#1^#(nil(), @l2, @l3) -> c_10()
, 13: zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
, 14: zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 12: zip3#1^#(nil(), @l2, @l3) -> c_10()
, 13: zip3#2^#(nil(), @l3, @x, @xs) -> c_12()
, 14: zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14()
, 10: group3#2^#(nil(), @x) -> c_5()
, 11: group3#3^#(nil(), @x, @y) -> c_7() }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict DPs:
{ group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Weak DPs: { group3^#(@l) -> group3#1^#(@l) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
We employ 'linear path analysis' using the following approximated
dependency graph:
->2:{1,9,4,3} [ ? ]
|
`->3:{2} [ YES(O(1),O(n^1)) ]
->1:{5,8,7,6} [ YES(O(1),O(n^1)) ]
Here dependency-pairs are as follows:
Strict DPs:
{ 1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, 2: group3#1^#(nil()) -> c_3()
, 3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, 4: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, 5: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, 6: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, 7: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, 8: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Weak DPs:
{ 9: group3^#(@l) -> group3#1^#(@l) }
* Path 2:{1,9,4,3}->3:{2}: YES(O(1),O(n^1))
-----------------------------------------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
Weak DPs: { group3^#(@l) -> group3#1^#(@l) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We consider the (estimated) dependency graph
1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
-->_1 group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y) :3
2: group3#1^#(nil()) -> c_3()
3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
-->_1 group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) :4
4: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
-->_1 group3^#(@l) -> group3#1^#(@l) :5
5: group3^#(@l) -> group3#1^#(@l)
-->_1 group3#1^#(nil()) -> c_3() :2
-->_1 group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {4} and add Pre({4}) = {3} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y) }
Weak DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We consider the (estimated) dependency graph
1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
-->_1 group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y) :3
2: group3#1^#(nil()) -> c_3()
3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
-->_1 group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) :5
4: group3^#(@l) -> group3#1^#(@l)
-->_1 group3#1^#(nil()) -> c_3() :2
-->_1 group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) :1
5: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
-->_1 group3^#(@l) -> group3#1^#(@l) :4
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {1} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#1^#(nil()) -> c_3() }
Weak DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 2: group3#1^#(nil()) -> c_3() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(::) = {}, Uargs(tuple#3) = {}, Uargs(group3^#) = {},
Uargs(group3#1^#) = {}, Uargs(group3#2^#) = {},
Uargs(group3#3^#) = {}, Uargs(zip3^#) = {}, Uargs(zip3#1^#) = {},
Uargs(zip3#2^#) = {}, Uargs(zip3#3^#) = {}
TcT has computed following constructor-restricted matrix
interpretation. Note that the diagonal of the component-wise maxima
of interpretation-entries (of constructors) contains no more than 0
non-zero entries.
[::](x1, x2) = [0]
[nil] = [0]
[tuple#3](x1, x2, x3) = [0]
[group3^#](x1) = [1]
[group3#1^#](x1) = [1]
[group3#2^#](x1, x2) = [1]
[c_3] = [0]
[group3#3^#](x1, x2, x3) = [1]
[zip3^#](x1, x2, x3) = [0]
[zip3#1^#](x1, x2, x3) = [0]
[zip3#2^#](x1, x2, x3, x4) = [0]
[zip3#3^#](x1, x2, x3, x4, x5) = [0]
This order satisfies following ordering constraints
[group3^#(@l)] = [1]
>= [1]
= [group3#1^#(@l)]
[group3#1^#(::(@x, @xs))] = [1]
>= [1]
= [group3#2^#(@xs, @x)]
[group3#1^#(nil())] = [1]
> [0]
= [c_3()]
[group3#2^#(::(@y, @ys), @x)] = [1]
>= [1]
= [group3#3^#(@ys, @x, @y)]
[group3#3^#(::(@z, @zs), @x, @y)] = [1]
>= [1]
= [group3^#(@zs)]
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(1)) on application of rules {2}.
Here rules are labeled according to the (estimated) dependency
graph
1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
-->_1 group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y) :4
2: group3#1^#(nil()) -> c_3()
3: group3^#(@l) -> group3#1^#(@l)
-->_1 group3#1^#(nil()) -> c_3() :2
-->_1 group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) :1
4: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
-->_1 group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) :5
5: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
-->_1 group3^#(@l) -> group3#1^#(@l) :3
Overall, we obtain that the number of applications of rules {2} is
given by YES(?,O(1)).
We apply the transformation 'removetails' on the sub-problem:
Strict DPs: { group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) }
Weak DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#1^#(nil()) -> c_3()
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{1,2,5,4}
|
`->2:{3} Weak SCC
Here dependency-pairs are as follows:
Strict DPs:
{ 1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) }
Weak DPs:
{ 2: group3^#(@l) -> group3#1^#(@l)
, 3: group3#1^#(nil()) -> c_3()
, 4: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, 5: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 3: group3#1^#(nil()) -> c_3() }
We apply the transformation 'simpKP' on the sub-problem:
Strict DPs: { group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) }
Weak DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
StartTerms: basic terms
Strategy: innermost
We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
to orient following rules strictly.
DPs:
{ 1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, 3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, 4: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
Sub-proof:
----------
The input was oriented with the instance of 'Small Polynomial Path
Order (PS,1-bounded)' as induced by the safe mapping
safe(::) = {1, 2}, safe(nil) = {}, safe(tuple#3) = {1, 2, 3},
safe(group3^#) = {}, safe(group3#1^#) = {}, safe(group3#2^#) = {},
safe(c_3) = {}, safe(group3#3^#) = {3}, safe(zip3^#) = {},
safe(zip3#1^#) = {}, safe(zip3#2^#) = {}, safe(zip3#3^#) = {}
and precedence
group3#2^# > group3#3^# .
Following symbols are considered recursive:
{}
The recursion depth is 0.
Further, following argument filtering is employed:
pi(::) = [2], pi(nil) = [], pi(tuple#3) = [], pi(group3^#) = 1,
pi(group3#1^#) = 1, pi(group3#2^#) = 1, pi(c_3) = [],
pi(group3#3^#) = 1, pi(zip3^#) = [], pi(zip3#1^#) = [],
pi(zip3#2^#) = [], pi(zip3#3^#) = []
Usable defined function symbols are a subset of:
{}
For your convenience, here are the satisfied ordering constraints:
pi(group3^#(@l)) = @l
>= @l
= pi(group3#1^#(@l))
pi(group3#1^#(::(@x, @xs))) = ::(; @xs)
> @xs
= pi(group3#2^#(@xs, @x))
pi(group3#2^#(::(@y, @ys), @x)) = ::(; @ys)
> @ys
= pi(group3#3^#(@ys, @x, @y))
pi(group3#3^#(::(@z, @zs), @x, @y)) = ::(; @zs)
> @zs
= pi(group3^#(@zs))
Processor 'Small Polynomial Path Order (PS,1-bounded)' induces the
complexity certificate YES(?,O(n^1)) on application of rules
{1,3,4}. Here rules are labeled according to the (estimated)
dependency graph
1: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
-->_1 group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y) :3
2: group3^#(@l) -> group3#1^#(@l)
-->_1 group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) :1
3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
-->_1 group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) :4
4: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
-->_1 group3^#(@l) -> group3#1^#(@l) :2
- The rules {1,3,4} have known complexity. These cover all
predecessors of {2}, their complexity is equally bounded.
Overall, we obtain that the number of applications of rules
{1,2,3,4} is given by YES(?,O(n^1)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ group3^#(@l) -> group3#1^#(@l)
, group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{1,4,3,2} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: group3^#(@l) -> group3#1^#(@l)
, 2: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x)
, 3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, 4: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 1: group3^#(@l) -> group3#1^#(@l)
, 4: group3#3^#(::(@z, @zs), @x, @y) -> group3^#(@zs)
, 3: group3#2^#(::(@y, @ys), @x) -> group3#3^#(@ys, @x, @y)
, 2: group3#1^#(::(@x, @xs)) -> group3#2^#(@xs, @x) }
We apply the transformation 'usablerules' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We apply the transformation 'trivial' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We consider the dependency graph
empty
All SCCs are trivial and dependency pairs can be removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
* Path 1:{5,8,7,6}: YES(O(1),O(n^1))
----------------------------------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We consider the (estimated) dependency graph
1: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
-->_1 zip3#1^#(::(@x, @xs), @l2, @l3) ->
zip3#2^#(@l2, @l3, @x, @xs) :2
2: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
-->_1 zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys) :3
3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
-->_1 zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) :4
4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
-->_1 zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {4} and add Pre({4}) = {3} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys) }
Weak DPs:
{ zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We consider the (estimated) dependency graph
1: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
-->_1 zip3#1^#(::(@x, @xs), @l2, @l3) ->
zip3#2^#(@l2, @l3, @x, @xs) :2
2: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
-->_1 zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys) :3
3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
-->_1 zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) :4
4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
-->_1 zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {2} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs) }
Weak DPs:
{ zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We consider the (estimated) dependency graph
1: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
-->_1 zip3#1^#(::(@x, @xs), @l2, @l3) ->
zip3#2^#(@l2, @l3, @x, @xs) :2
2: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
-->_1 zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys) :3
3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
-->_1 zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) :4
4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
-->_1 zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {2} and add Pre({2}) = {1} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3) }
Weak DPs:
{ zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
to orient following rules strictly.
DPs:
{ 4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
Sub-proof:
----------
The input was oriented with the instance of 'Small Polynomial Path
Order (PS,1-bounded)' as induced by the safe mapping
safe(::) = {1, 2}, safe(nil) = {}, safe(tuple#3) = {1, 2, 3},
safe(group3^#) = {}, safe(group3#1^#) = {}, safe(group3#2^#) = {},
safe(group3#3^#) = {}, safe(zip3^#) = {}, safe(zip3#1^#) = {1},
safe(zip3#2^#) = {2}, safe(zip3#3^#) = {}
and precedence
empty .
Following symbols are considered recursive:
{}
The recursion depth is 0.
Further, following argument filtering is employed:
pi(::) = [2], pi(nil) = [], pi(tuple#3) = [], pi(group3^#) = [],
pi(group3#1^#) = [], pi(group3#2^#) = [], pi(group3#3^#) = [],
pi(zip3^#) = 3, pi(zip3#1^#) = 3, pi(zip3#2^#) = 2,
pi(zip3#3^#) = 1
Usable defined function symbols are a subset of:
{}
For your convenience, here are the satisfied ordering constraints:
pi(zip3^#(@l1, @l2, @l3)) = @l3
>= @l3
= pi(zip3#1^#(@l1, @l2, @l3))
pi(zip3#1^#(::(@x, @xs), @l2, @l3)) = @l3
>= @l3
= pi(zip3#2^#(@l2, @l3, @x, @xs))
pi(zip3#2^#(::(@y, @ys), @l3, @x, @xs)) = @l3
>= @l3
= pi(zip3#3^#(@l3, @x, @xs, @y, @ys))
pi(zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys)) = ::(; @zs)
> @zs
= pi(zip3^#(@xs, @ys, @zs))
Processor 'Small Polynomial Path Order (PS,1-bounded)' induces the
complexity certificate YES(?,O(n^1)) on application of rules {4}.
Here rules are labeled according to the (estimated) dependency
graph
1: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
-->_1 zip3#1^#(::(@x, @xs), @l2, @l3) ->
zip3#2^#(@l2, @l3, @x, @xs) :2
2: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
-->_1 zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys) :3
3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
-->_1 zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) :4
4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> zip3^#(@xs, @ys, @zs)
-->_1 zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3) :1
- The rules {4} have known complexity. These cover all predecessors
of {1}, their complexity is equally bounded.
- The rules {1,4} have known complexity. These cover all
predecessors of {2}, their complexity is equally bounded.
- The rules {1,2,4} have known complexity. These cover all
predecessors of {3}, their complexity is equally bounded.
Overall, we obtain that the number of applications of rules
{1,2,3,4} is given by YES(?,O(n^1)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{1,4,3,2} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, 2: zip3#1^#(::(@x, @xs), @l2, @l3) -> zip3#2^#(@l2, @l3, @x, @xs)
, 3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, 4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 1: zip3^#(@l1, @l2, @l3) -> zip3#1^#(@l1, @l2, @l3)
, 4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) ->
zip3^#(@xs, @ys, @zs)
, 3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) ->
zip3#3^#(@l3, @x, @xs, @y, @ys)
, 2: zip3#1^#(::(@x, @xs), @l2, @l3) ->
zip3#2^#(@l2, @l3, @x, @xs) }
We apply the transformation 'usablerules' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We apply the transformation 'trivial' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We consider the dependency graph
empty
All SCCs are trivial and dependency pairs can be removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^1))