We consider the following Problem:
Strict Trs:
{ concat(leaf(), Y) -> Y
, concat(cons(U, V), Y) -> cons(U, concat(V, Y))
, lessleaves(X, leaf()) -> false()
, lessleaves(leaf(), cons(W, Z)) -> true()
, lessleaves(cons(U, V), cons(W, Z)) ->
lessleaves(concat(U, V), concat(W, Z))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ concat(leaf(), Y) -> Y
, concat(cons(U, V), Y) -> cons(U, concat(V, Y))
, lessleaves(X, leaf()) -> false()
, lessleaves(leaf(), cons(W, Z)) -> true()
, lessleaves(cons(U, V), cons(W, Z)) ->
lessleaves(concat(U, V), concat(W, Z))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ lessleaves(X, leaf()) -> false()
, lessleaves(leaf(), cons(W, Z)) -> true()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(concat) = {}, Uargs(cons) = {2}, Uargs(lessleaves) = {1, 2}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
concat(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
leaf() = [1]
[0]
cons(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [1 0] [3]
lessleaves(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [3]
false() = [0]
[0]
true() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ concat(leaf(), Y) -> Y
, concat(cons(U, V), Y) -> cons(U, concat(V, Y))
, lessleaves(cons(U, V), cons(W, Z)) ->
lessleaves(concat(U, V), concat(W, Z))}
Weak Trs:
{ lessleaves(X, leaf()) -> false()
, lessleaves(leaf(), cons(W, Z)) -> true()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {concat(leaf(), Y) -> Y}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(concat) = {}, Uargs(cons) = {2}, Uargs(lessleaves) = {1, 2}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
concat(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
leaf() = [0]
[0]
cons(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [1 0] [0]
lessleaves(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
false() = [0]
[0]
true() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ concat(cons(U, V), Y) -> cons(U, concat(V, Y))
, lessleaves(cons(U, V), cons(W, Z)) ->
lessleaves(concat(U, V), concat(W, Z))}
Weak Trs:
{ concat(leaf(), Y) -> Y
, lessleaves(X, leaf()) -> false()
, lessleaves(leaf(), cons(W, Z)) -> true()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{lessleaves(cons(U, V), cons(W, Z)) ->
lessleaves(concat(U, V), concat(W, Z))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(concat) = {}, Uargs(cons) = {2}, Uargs(lessleaves) = {1, 2}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
concat(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
leaf() = [0]
[0]
cons(x1, x2) = [0 0] x1 + [1 0] x2 + [2]
[0 0] [1 0] [0]
lessleaves(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
false() = [0]
[0]
true() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {concat(cons(U, V), Y) -> cons(U, concat(V, Y))}
Weak Trs:
{ lessleaves(cons(U, V), cons(W, Z)) ->
lessleaves(concat(U, V), concat(W, Z))
, concat(leaf(), Y) -> Y
, lessleaves(X, leaf()) -> false()
, lessleaves(leaf(), cons(W, Z)) -> true()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {concat(cons(U, V), Y) -> cons(U, concat(V, Y))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(concat) = {}, Uargs(cons) = {2}, Uargs(lessleaves) = {1, 2}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
concat(x1, x2) = [0 1] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
leaf() = [0]
[0]
cons(x1, x2) = [0 1] x1 + [1 0] x2 + [0]
[0 1] [0 1] [1]
lessleaves(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
false() = [0]
[0]
true() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Weak Trs:
{ concat(cons(U, V), Y) -> cons(U, concat(V, Y))
, lessleaves(cons(U, V), cons(W, Z)) ->
lessleaves(concat(U, V), concat(W, Z))
, concat(leaf(), Y) -> Y
, lessleaves(X, leaf()) -> false()
, lessleaves(leaf(), cons(W, Z)) -> true()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ concat(cons(U, V), Y) -> cons(U, concat(V, Y))
, lessleaves(cons(U, V), cons(W, Z)) ->
lessleaves(concat(U, V), concat(W, Z))
, concat(leaf(), Y) -> Y
, lessleaves(X, leaf()) -> false()
, lessleaves(leaf(), cons(W, Z)) -> true()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))