tct
| Execution Time (secs) | 2.918 |
| Answer | YES(O(1),O(n^2)) |
| Input | subtrees.raml |
YES(O(1),O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We add following dependency tuples
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, append#1^#(nil(), @l2) -> c_3()
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(leaf()) -> c_5()
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
and replace the set of basic marked basic terms accordingly.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, append#1^#(nil(), @l2) -> c_3()
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(leaf()) -> c_5()
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :2
-->_1 append#1^#(nil(), @l2) -> c_3() :3
2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
3: append#1^#(nil(), @l2) -> c_3()
4: subtrees^#(@t) -> subtrees#1^#(@t)
-->_1 subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) :6
-->_1 subtrees#1^#(leaf()) -> c_5() :5
5: subtrees#1^#(leaf()) -> c_5()
6: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
-->_1 subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2)) :7
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :4
7: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
-->_1 subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) :8
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :4
8: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {5} and add Pre({5}) = {4} to the strict component.
- 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^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak DPs:
{ append#1^#(nil(), @l2) -> c_3()
, subtrees#1^#(leaf()) -> c_5() }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the the dependency graph
->1:{3,5,4}
|
|->3:{6}
| |
| `->4:{1,2}
| |
| `->5:{7} Weak SCC
|
`->2:{8} Weak SCC
Here dependency-pairs are as follows:
Strict DPs:
{ 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, 2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, 3: subtrees^#(@t) -> subtrees#1^#(@t)
, 4: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, 5: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, 6: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak DPs:
{ 7: append#1^#(nil(), @l2) -> c_3()
, 8: subtrees#1^#(leaf()) -> c_5() }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 8: subtrees#1^#(leaf()) -> c_5()
, 7: append#1^#(nil(), @l2) -> c_3() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :2
2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
3: subtrees^#(@t) -> subtrees#1^#(@t)
-->_1 subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) :4
4: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
-->_1 subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2)) :5
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :3
5: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
-->_1 subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) :6
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :3
6: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :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^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak DPs: { append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :6
2: subtrees^#(@t) -> subtrees#1^#(@t)
-->_1 subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) :3
3: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
-->_1 subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2)) :4
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
4: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
-->_1 subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) :5
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
5: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
6: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {5} and add Pre({5}) = {4} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2)) }
Weak DPs:
{ append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :5
2: subtrees^#(@t) -> subtrees#1^#(@t)
-->_1 subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) :3
3: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
-->_1 subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2)) :4
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
4: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
-->_1 subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) :6
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
5: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
6: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :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^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) }
Weak DPs:
{ append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :4
2: subtrees^#(@t) -> subtrees#1^#(@t)
-->_1 subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) :3
3: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
-->_1 subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2)) :5
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
4: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
5: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
-->_1 subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) :6
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
6: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :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^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, subtrees^#(@t) -> subtrees#1^#(@t) }
Weak DPs:
{ append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
DPs:
{ 3: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, 4: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) }
Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, subtrees(@t) -> subtrees#1(@t) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(append) = {}, Uargs(append#1) = {}, Uargs(::) = {},
Uargs(subtrees) = {}, Uargs(subtrees#1) = {}, Uargs(node) = {},
Uargs(subtrees#2) = {}, Uargs(subtrees#3) = {},
Uargs(append^#) = {}, Uargs(append#1^#) = {},
Uargs(subtrees^#) = {}, Uargs(subtrees#1^#) = {},
Uargs(c_6) = {1, 2}, Uargs(subtrees#2^#) = {}, Uargs(c_7) = {1, 2},
Uargs(subtrees#3^#) = {}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[append](x1, x2) = [3 0] x1 + [1 2] x2 + [2]
[0 1] [0 1] [0]
[append#1](x1, x2) = [2 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
[::](x1, x2) = [0 0] x2 + [0]
[0 1] [1]
[nil] = [0]
[0]
[subtrees](x1) = [0 0] x1 + [1]
[1 0] [0]
[subtrees#1](x1) = [0 0] x1 + [0]
[1 0] [0]
[leaf] = [0]
[0]
[node](x1, x2, x3) = [0 0] x1 + [1 0] x2 + [1
0] x3 + [2]
[0 1] [1 1] [0
1] [2]
[subtrees#2](x1, x2, x3, x4) = [0 0] x1 + [0 0] x3 + [0]
[1 1] [1 0] [1]
[subtrees#3](x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [1]
[append^#](x1, x2) = [0 1] x1 + [0]
[0 0] [0]
[append#1^#](x1, x2) = [0 1] x1 + [0]
[0 0] [0]
[subtrees^#](x1) = [0 2] x1 + [0]
[0 0] [0]
[subtrees#1^#](x1) = [0 2] x1 + [0]
[0 0] [0]
[c_6](x1, x2) = [1 0] x1 + [1 1] x2 + [0]
[0 0] [0 0] [0]
[subtrees#2^#](x1, x2, x3, x4) = [3 2] x1 + [0 2] x3 + [0]
[1 0] [1 0] [1]
[c_7](x1, x2) = [2 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[subtrees#3^#](x1, x2, x3, x4, x5) = [0 0] x1 + [0 1] x2 + [0]
[0 1] [0 0] [0]
This order satisfies following ordering constraints
[append(@l1, @l2)] = [3 0] @l1 + [1 2] @l2 + [2]
[0 1] [0 1] [0]
> [2 0] @l1 + [1 0] @l2 + [0]
[0 1] [0 1] [0]
= [append#1(@l1, @l2)]
[append#1(::(@x, @xs), @l2)] = [1 0] @l2 + [0 0] @xs + [0]
[0 1] [0 1] [1]
>= [0 0] @l2 + [0 0] @xs + [0]
[0 1] [0 1] [1]
= [::(@x, append(@xs, @l2))]
[append#1(nil(), @l2)] = [1 0] @l2 + [0]
[0 1] [0]
>= [1 0] @l2 + [0]
[0 1] [0]
= [@l2]
[subtrees(@t)] = [0 0] @t + [1]
[1 0] [0]
> [0 0] @t + [0]
[1 0] [0]
= [subtrees#1(@t)]
[subtrees#1(leaf())] = [0]
[0]
>= [0]
[0]
= [nil()]
[subtrees#1(node(@x, @t1, @t2))] = [0 0] @t1 + [0 0] @t2 + [0]
[1 0] [1 0] [2]
>= [0 0] @t1 + [0 0] @t2 + [0]
[1 0] [1 0] [2]
= [subtrees#2(subtrees(@t1), @t1, @t2, @x)]
[subtrees#2(@l1, @t1, @t2, @x)] = [0 0] @l1 + [0 0] @t2 + [0]
[1 1] [1 0] [1]
>= [0 0] @l1 + [0 0] @t2 + [0]
[0 1] [1 0] [1]
= [subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)]
[subtrees#3(@l2, @l1, @t1, @t2, @x)] = [0 0] @l1 + [0 0] @l2 + [0]
[0 1] [0 1] [1]
>= [0 0] @l1 + [0 0] @l2 + [0]
[0 1] [0 1] [1]
= [::(node(@x, @t1, @t2), append(@l1, @l2))]
[append^#(@l1, @l2)] = [0 1] @l1 + [0]
[0 0] [0]
>= [0 1] @l1 + [0]
[0 0] [0]
= [append#1^#(@l1, @l2)]
[append#1^#(::(@x, @xs), @l2)] = [0 1] @xs + [1]
[0 0] [0]
> [0 1] @xs + [0]
[0 0] [0]
= [append^#(@xs, @l2)]
[subtrees^#(@t)] = [0 2] @t + [0]
[0 0] [0]
>= [0 2] @t + [0]
[0 0] [0]
= [subtrees#1^#(@t)]
[subtrees#1^#(node(@x, @t1, @t2))] = [2 2] @t1 + [0 2] @t2 + [0 2] @x + [4]
[0 0] [0 0] [0 0] [0]
> [2 2] @t1 + [0 2] @t2 + [3]
[0 0] [0 0] [0]
= [c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))]
[subtrees#2^#(@l1, @t1, @t2, @x)] = [3 2] @l1 + [0 2] @t2 + [0]
[1 0] [1 0] [1]
>= [0 2] @l1 + [0 2] @t2 + [0]
[0 0] [0 0] [0]
= [c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))]
[subtrees#3^#(@l2, @l1, @t1, @t2, @x)] = [0 1] @l1 + [0 0] @l2 + [0]
[0 0] [0 1] [0]
>= [0 1] @l1 + [0]
[0 0] [0]
= [append^#(@l1, @l2)]
Processor 'matrix interpretation of dimension 2' induces the
complexity certificate YES(?,O(n^2)) on application of rules {3,4}.
Here rules are labeled according to the (estimated) dependency
graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :3
2: subtrees^#(@t) -> subtrees#1^#(@t)
-->_1 subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) :4
3: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
4: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
-->_1 subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2)) :5
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
5: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
-->_1 subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) :6
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
6: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
- The rules {3,4} have known complexity. These cover all
predecessors of {5}, their complexity is equally bounded.
- The rules {3,4,5} have known complexity. These cover all
predecessors of {2,6}, their complexity is equally bounded.
- The rules {2,3,4,5,6} have known complexity. These cover all
predecessors of {1}, their complexity is equally bounded.
Overall, we obtain that the number of applications of rules
{1,2,3,4,5,6} is given by YES(?,O(n^2)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{3,5,4} Weak SCC
|
`->2:{6} Weak SCC
|
`->3:{1,2} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, 2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, 3: subtrees^#(@t) -> subtrees#1^#(@t)
, 4: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, 5: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, 6: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 3: subtrees^#(@t) -> subtrees#1^#(@t)
, 5: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, 4: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, 6: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2)
, 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, 2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) }
We apply the transformation 'usablerules' on the sub-problem:
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
StartTerms: basic terms
Strategy: innermost
No rule is usable.
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^2))
tct-popstar
| Execution Time (secs) | 3.231 |
| Answer | YES(O(1),O(n^2)) |
| Input | subtrees.raml |
YES(O(1),O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We add following dependency tuples
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, append#1^#(nil(), @l2) -> c_3()
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(leaf()) -> c_5()
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
and replace the set of basic marked basic terms accordingly.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, append#1^#(nil(), @l2) -> c_3()
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(leaf()) -> c_5()
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :2
-->_1 append#1^#(nil(), @l2) -> c_3() :3
2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
3: append#1^#(nil(), @l2) -> c_3()
4: subtrees^#(@t) -> subtrees#1^#(@t)
-->_1 subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) :6
-->_1 subtrees#1^#(leaf()) -> c_5() :5
5: subtrees#1^#(leaf()) -> c_5()
6: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
-->_1 subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2)) :7
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :4
7: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
-->_1 subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) :8
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :4
8: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {5} and add Pre({5}) = {4} to the strict component.
- 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^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak DPs:
{ append#1^#(nil(), @l2) -> c_3()
, subtrees#1^#(leaf()) -> c_5() }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the the dependency graph
->1:{3,5,4}
|
|->3:{6}
| |
| `->4:{1,2}
| |
| `->5:{7} Weak SCC
|
`->2:{8} Weak SCC
Here dependency-pairs are as follows:
Strict DPs:
{ 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, 2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, 3: subtrees^#(@t) -> subtrees#1^#(@t)
, 4: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, 5: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, 6: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak DPs:
{ 7: append#1^#(nil(), @l2) -> c_3()
, 8: subtrees#1^#(leaf()) -> c_5() }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 8: subtrees#1^#(leaf()) -> c_5()
, 7: append#1^#(nil(), @l2) -> c_3() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :2
2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
3: subtrees^#(@t) -> subtrees#1^#(@t)
-->_1 subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) :4
4: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
-->_1 subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2)) :5
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :3
5: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
-->_1 subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) :6
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :3
6: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :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^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak DPs: { append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :6
2: subtrees^#(@t) -> subtrees#1^#(@t)
-->_1 subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) :3
3: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
-->_1 subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2)) :4
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
4: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
-->_1 subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) :5
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
5: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
6: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {5} and add Pre({5}) = {4} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2)) }
Weak DPs:
{ append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :5
2: subtrees^#(@t) -> subtrees#1^#(@t)
-->_1 subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) :3
3: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
-->_1 subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2)) :4
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
4: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
-->_1 subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) :6
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
5: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
6: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :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^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) }
Weak DPs:
{ append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :4
2: subtrees^#(@t) -> subtrees#1^#(@t)
-->_1 subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) :3
3: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
-->_1 subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2)) :5
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
4: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
5: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
-->_1 subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) :6
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
6: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :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^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, subtrees^#(@t) -> subtrees#1^#(@t) }
Weak DPs:
{ append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
DPs:
{ 3: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, 4: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) }
Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, subtrees(@t) -> subtrees#1(@t) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(append) = {}, Uargs(append#1) = {}, Uargs(::) = {},
Uargs(subtrees) = {}, Uargs(subtrees#1) = {}, Uargs(node) = {},
Uargs(subtrees#2) = {}, Uargs(subtrees#3) = {},
Uargs(append^#) = {}, Uargs(append#1^#) = {},
Uargs(subtrees^#) = {}, Uargs(subtrees#1^#) = {},
Uargs(c_6) = {1, 2}, Uargs(subtrees#2^#) = {}, Uargs(c_7) = {1, 2},
Uargs(subtrees#3^#) = {}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[append](x1, x2) = [3 0] x1 + [1 2] x2 + [2]
[0 1] [0 1] [0]
[append#1](x1, x2) = [2 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
[::](x1, x2) = [0 0] x2 + [0]
[0 1] [1]
[nil] = [0]
[0]
[subtrees](x1) = [0 0] x1 + [1]
[1 0] [0]
[subtrees#1](x1) = [0 0] x1 + [0]
[1 0] [0]
[leaf] = [0]
[0]
[node](x1, x2, x3) = [0 0] x1 + [1 0] x2 + [1
0] x3 + [2]
[0 1] [1 1] [0
1] [2]
[subtrees#2](x1, x2, x3, x4) = [0 0] x1 + [0 0] x3 + [0]
[1 1] [1 0] [1]
[subtrees#3](x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [1]
[append^#](x1, x2) = [0 1] x1 + [0]
[0 0] [0]
[append#1^#](x1, x2) = [0 1] x1 + [0]
[0 0] [0]
[subtrees^#](x1) = [0 2] x1 + [0]
[0 0] [0]
[subtrees#1^#](x1) = [0 2] x1 + [0]
[0 0] [0]
[c_6](x1, x2) = [1 0] x1 + [1 1] x2 + [0]
[0 0] [0 0] [0]
[subtrees#2^#](x1, x2, x3, x4) = [3 2] x1 + [0 2] x3 + [0]
[1 0] [1 0] [1]
[c_7](x1, x2) = [2 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[subtrees#3^#](x1, x2, x3, x4, x5) = [0 0] x1 + [0 1] x2 + [0]
[0 1] [0 0] [0]
This order satisfies following ordering constraints
[append(@l1, @l2)] = [3 0] @l1 + [1 2] @l2 + [2]
[0 1] [0 1] [0]
> [2 0] @l1 + [1 0] @l2 + [0]
[0 1] [0 1] [0]
= [append#1(@l1, @l2)]
[append#1(::(@x, @xs), @l2)] = [1 0] @l2 + [0 0] @xs + [0]
[0 1] [0 1] [1]
>= [0 0] @l2 + [0 0] @xs + [0]
[0 1] [0 1] [1]
= [::(@x, append(@xs, @l2))]
[append#1(nil(), @l2)] = [1 0] @l2 + [0]
[0 1] [0]
>= [1 0] @l2 + [0]
[0 1] [0]
= [@l2]
[subtrees(@t)] = [0 0] @t + [1]
[1 0] [0]
> [0 0] @t + [0]
[1 0] [0]
= [subtrees#1(@t)]
[subtrees#1(leaf())] = [0]
[0]
>= [0]
[0]
= [nil()]
[subtrees#1(node(@x, @t1, @t2))] = [0 0] @t1 + [0 0] @t2 + [0]
[1 0] [1 0] [2]
>= [0 0] @t1 + [0 0] @t2 + [0]
[1 0] [1 0] [2]
= [subtrees#2(subtrees(@t1), @t1, @t2, @x)]
[subtrees#2(@l1, @t1, @t2, @x)] = [0 0] @l1 + [0 0] @t2 + [0]
[1 1] [1 0] [1]
>= [0 0] @l1 + [0 0] @t2 + [0]
[0 1] [1 0] [1]
= [subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)]
[subtrees#3(@l2, @l1, @t1, @t2, @x)] = [0 0] @l1 + [0 0] @l2 + [0]
[0 1] [0 1] [1]
>= [0 0] @l1 + [0 0] @l2 + [0]
[0 1] [0 1] [1]
= [::(node(@x, @t1, @t2), append(@l1, @l2))]
[append^#(@l1, @l2)] = [0 1] @l1 + [0]
[0 0] [0]
>= [0 1] @l1 + [0]
[0 0] [0]
= [append#1^#(@l1, @l2)]
[append#1^#(::(@x, @xs), @l2)] = [0 1] @xs + [1]
[0 0] [0]
> [0 1] @xs + [0]
[0 0] [0]
= [append^#(@xs, @l2)]
[subtrees^#(@t)] = [0 2] @t + [0]
[0 0] [0]
>= [0 2] @t + [0]
[0 0] [0]
= [subtrees#1^#(@t)]
[subtrees#1^#(node(@x, @t1, @t2))] = [2 2] @t1 + [0 2] @t2 + [0 2] @x + [4]
[0 0] [0 0] [0 0] [0]
> [2 2] @t1 + [0 2] @t2 + [3]
[0 0] [0 0] [0]
= [c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))]
[subtrees#2^#(@l1, @t1, @t2, @x)] = [3 2] @l1 + [0 2] @t2 + [0]
[1 0] [1 0] [1]
>= [0 2] @l1 + [0 2] @t2 + [0]
[0 0] [0 0] [0]
= [c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))]
[subtrees#3^#(@l2, @l1, @t1, @t2, @x)] = [0 1] @l1 + [0 0] @l2 + [0]
[0 0] [0 1] [0]
>= [0 1] @l1 + [0]
[0 0] [0]
= [append^#(@l1, @l2)]
Processor 'matrix interpretation of dimension 2' induces the
complexity certificate YES(?,O(n^2)) on application of rules {3,4}.
Here rules are labeled according to the (estimated) dependency
graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :3
2: subtrees^#(@t) -> subtrees#1^#(@t)
-->_1 subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1)) :4
3: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
4: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
-->_1 subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2)) :5
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
5: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
-->_1 subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) :6
-->_2 subtrees^#(@t) -> subtrees#1^#(@t) :2
6: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
- The rules {3,4} have known complexity. These cover all
predecessors of {5}, their complexity is equally bounded.
- The rules {3,4,5} have known complexity. These cover all
predecessors of {2,6}, their complexity is equally bounded.
- The rules {2,3,4,5,6} have known complexity. These cover all
predecessors of {1}, their complexity is equally bounded.
Overall, we obtain that the number of applications of rules
{1,2,3,4,5,6} is given by YES(?,O(n^2)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, subtrees^#(@t) -> subtrees#1^#(@t)
, subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{3,5,4} Weak SCC
|
`->2:{6} Weak SCC
|
`->3:{1,2} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, 2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, 3: subtrees^#(@t) -> subtrees#1^#(@t)
, 4: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, 5: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, 6: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 3: subtrees^#(@t) -> subtrees#1^#(@t)
, 5: subtrees#2^#(@l1, @t1, @t2, @x) ->
c_7(subtrees#3^#(subtrees(@t2), @l1, @t1, @t2, @x),
subtrees^#(@t2))
, 4: subtrees#1^#(node(@x, @t1, @t2)) ->
c_6(subtrees#2^#(subtrees(@t1), @t1, @t2, @x), subtrees^#(@t1))
, 6: subtrees#3^#(@l2, @l1, @t1, @t2, @x) -> append^#(@l1, @l2)
, 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, 2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) }
We apply the transformation 'usablerules' on the sub-problem:
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, subtrees(@t) -> subtrees#1(@t)
, subtrees#1(leaf()) -> nil()
, subtrees#1(node(@x, @t1, @t2)) ->
subtrees#2(subtrees(@t1), @t1, @t2, @x)
, subtrees#2(@l1, @t1, @t2, @x) ->
subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
, subtrees#3(@l2, @l1, @t1, @t2, @x) ->
::(node(@x, @t1, @t2), append(@l1, @l2)) }
StartTerms: basic terms
Strategy: innermost
No rule is usable.
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^2))