We consider the following Problem:
Strict Trs:
{ f(node(s(n), xs)) -> f(addchild(select(xs), node(n, xs)))
, select(cons(ap, xs)) -> ap
, select(cons(ap, xs)) -> select(xs)
, addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ f(node(s(n), xs)) -> f(addchild(select(xs), node(n, xs)))
, select(cons(ap, xs)) -> ap
, select(cons(ap, xs)) -> select(xs)
, addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {select(cons(ap, xs)) -> select(xs)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {1}, Uargs(node) = {}, Uargs(s) = {},
Uargs(addchild) = {1}, Uargs(select) = {}, Uargs(cons) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1) = [1 0] x1 + [1]
[0 0] [1]
node(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
addchild(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
select(x1) = [1 0] x1 + [0]
[0 0] [1]
cons(x1, x2) = [0 0] x1 + [1 0] x2 + [2]
[0 0] [0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ f(node(s(n), xs)) -> f(addchild(select(xs), node(n, xs)))
, select(cons(ap, xs)) -> ap
, addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))}
Weak Trs: {select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {1}, Uargs(node) = {}, Uargs(s) = {},
Uargs(addchild) = {1}, Uargs(select) = {}, Uargs(cons) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1) = [1 0] x1 + [1]
[0 0] [1]
node(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
addchild(x1, x2) = [1 0] x1 + [0 0] x2 + [2]
[0 0] [0 0] [1]
select(x1) = [1 0] x1 + [2]
[0 0] [1]
cons(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ f(node(s(n), xs)) -> f(addchild(select(xs), node(n, xs)))
, select(cons(ap, xs)) -> ap}
Weak Trs:
{ addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{f(node(s(n), xs)) -> f(addchild(select(xs), node(n, xs)))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {1}, Uargs(node) = {}, Uargs(s) = {},
Uargs(addchild) = {1}, Uargs(select) = {}, Uargs(cons) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1) = [1 0] x1 + [0]
[0 0] [0]
node(x1, x2) = [0 0] x1 + [1 0] x2 + [2]
[0 0] [0 0] [1]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
addchild(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
select(x1) = [1 0] x1 + [0]
[0 0] [1]
cons(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {select(cons(ap, xs)) -> ap}
Weak Trs:
{ f(node(s(n), xs)) -> f(addchild(select(xs), node(n, xs)))
, addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs: {select(cons(ap, xs)) -> ap}
Weak Trs:
{ f(node(s(n), xs)) -> f(addchild(select(xs), node(n, xs)))
, addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We have computed the following dependency pairs
Strict DPs: {select^#(cons(ap, xs)) -> c_1()}
Weak DPs:
{ f^#(node(s(n), xs)) -> f^#(addchild(select(xs), node(n, xs)))
, addchild^#(node(y, ys), node(n, xs)) -> c_3()
, select^#(cons(ap, xs)) -> select^#(xs)}
We consider the following Problem:
Strict DPs: {select^#(cons(ap, xs)) -> c_1()}
Strict Trs: {select(cons(ap, xs)) -> ap}
Weak DPs:
{ f^#(node(s(n), xs)) -> f^#(addchild(select(xs), node(n, xs)))
, addchild^#(node(y, ys), node(n, xs)) -> c_3()
, select^#(cons(ap, xs)) -> select^#(xs)}
Weak Trs:
{ f(node(s(n), xs)) -> f(addchild(select(xs), node(n, xs)))
, addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We replace strict/weak-rules by the corresponding usable rules:
Strict Usable Rules: {select(cons(ap, xs)) -> ap}
Weak Usable Rules:
{ addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
We consider the following Problem:
Strict DPs: {select^#(cons(ap, xs)) -> c_1()}
Strict Trs: {select(cons(ap, xs)) -> ap}
Weak DPs:
{ f^#(node(s(n), xs)) -> f^#(addchild(select(xs), node(n, xs)))
, addchild^#(node(y, ys), node(n, xs)) -> c_3()
, select^#(cons(ap, xs)) -> select^#(xs)}
Weak Trs:
{ addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict DPs: {select^#(cons(ap, xs)) -> c_1()}
Strict Trs: {select(cons(ap, xs)) -> ap}
Weak DPs:
{ f^#(node(s(n), xs)) -> f^#(addchild(select(xs), node(n, xs)))
, addchild^#(node(y, ys), node(n, xs)) -> c_3()
, select^#(cons(ap, xs)) -> select^#(xs)}
Weak Trs:
{ addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We use following congruence DG for path analysis
->3:{2} [ YES(O(1),O(1)) ]
->2:{3} [ YES(O(1),O(1)) ]
->1:{4} [ subsumed ]
|
`->4:{1} [ YES(?,O(n^1)) ]
Here dependency-pairs are as follows:
Strict DPs:
{1: select^#(cons(ap, xs)) -> c_1()}
WeakDPs DPs:
{ 2: f^#(node(s(n), xs)) -> f^#(addchild(select(xs), node(n, xs)))
, 3: addchild^#(node(y, ys), node(n, xs)) -> c_3()
, 4: select^#(cons(ap, xs)) -> select^#(xs)}
* Path 3:{2}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict Trs: {select(cons(ap, xs)) -> ap}
Weak Trs:
{ addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {select(cons(ap, xs)) -> ap}
Weak Trs:
{ addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {select(cons(ap, xs)) -> ap}
Weak Trs:
{ addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 2:{3}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict Trs: {select(cons(ap, xs)) -> ap}
Weak Trs:
{ addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {select(cons(ap, xs)) -> ap}
Weak Trs:
{ addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {select(cons(ap, xs)) -> ap}
Weak Trs:
{ addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 1:{4}: subsumed
--------------------
This path is subsumed by the proof of paths 1:{4}->4:{1}.
* Path 1:{4}->4:{1}: YES(?,O(n^1))
--------------------------------
We consider the following Problem:
Strict DPs: {select^#(cons(ap, xs)) -> c_1()}
Strict Trs: {select(cons(ap, xs)) -> ap}
Weak DPs: {select^#(cons(ap, xs)) -> select^#(xs)}
Weak Trs:
{ addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict DPs: {select^#(cons(ap, xs)) -> c_1()}
Strict Trs: {select(cons(ap, xs)) -> ap}
Weak DPs: {select^#(cons(ap, xs)) -> select^#(xs)}
Weak Trs:
{ addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict DPs: {select^#(cons(ap, xs)) -> c_1()}
Strict Trs: {select(cons(ap, xs)) -> ap}
Weak DPs: {select^#(cons(ap, xs)) -> select^#(xs)}
Weak Trs:
{ addchild(node(y, ys), node(n, xs)) ->
node(y, cons(node(n, xs), ys))
, select(cons(ap, xs)) -> select(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
No rule is usable.
We consider the following Problem:
Strict DPs: {select^#(cons(ap, xs)) -> c_1()}
Weak DPs: {select^#(cons(ap, xs)) -> select^#(xs)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ cons_0(2, 2) -> 2
, select^#_0(2) -> 1
, c_1_1() -> 1}
Hurray, we answered YES(?,O(n^1))