We consider the following Problem:
Strict Trs:
{ __(__(X, Y), Z) -> __(X, __(Y, Z))
, __(X, nil()) -> X
, __(nil(), X) -> X
, U11(tt()) -> U12(tt())
, U12(tt()) -> tt()
, isNePal(__(I, __(P, I))) -> U11(tt())
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ __(__(X, Y), Z) -> __(X, __(Y, Z))
, __(X, nil()) -> X
, __(nil(), X) -> X
, U11(tt()) -> U12(tt())
, U12(tt()) -> tt()
, isNePal(__(I, __(P, I))) -> U11(tt())
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {U12(tt()) -> tt()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {2}, Uargs(U11) = {}, Uargs(U12) = {},
Uargs(isNePal) = {}, Uargs(activate) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 0] [0]
nil() = [0]
[0]
U11(x1) = [0 0] x1 + [1]
[0 0] [1]
tt() = [0]
[0]
U12(x1) = [0 0] x1 + [1]
[0 0] [1]
isNePal(x1) = [0 0] x1 + [1]
[0 0] [1]
activate(x1) = [1 0] x1 + [0]
[0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ __(__(X, Y), Z) -> __(X, __(Y, Z))
, __(X, nil()) -> X
, __(nil(), X) -> X
, U11(tt()) -> U12(tt())
, isNePal(__(I, __(P, I))) -> U11(tt())
, activate(X) -> X}
Weak Trs: {U12(tt()) -> tt()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {activate(X) -> X}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {2}, Uargs(U11) = {}, Uargs(U12) = {},
Uargs(isNePal) = {}, Uargs(activate) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 0] [0]
nil() = [0]
[0]
U11(x1) = [0 0] x1 + [1]
[0 0] [1]
tt() = [0]
[0]
U12(x1) = [0 0] x1 + [1]
[0 0] [1]
isNePal(x1) = [0 0] x1 + [1]
[0 0] [1]
activate(x1) = [1 0] x1 + [2]
[0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ __(__(X, Y), Z) -> __(X, __(Y, Z))
, __(X, nil()) -> X
, __(nil(), X) -> X
, U11(tt()) -> U12(tt())
, isNePal(__(I, __(P, I))) -> U11(tt())}
Weak Trs:
{ activate(X) -> X
, U12(tt()) -> tt()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {isNePal(__(I, __(P, I))) -> U11(tt())}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {2}, Uargs(U11) = {}, Uargs(U12) = {},
Uargs(isNePal) = {}, Uargs(activate) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 0] [0]
nil() = [0]
[0]
U11(x1) = [0 0] x1 + [1]
[0 0] [1]
tt() = [0]
[0]
U12(x1) = [0 0] x1 + [1]
[0 0] [1]
isNePal(x1) = [0 0] x1 + [3]
[0 0] [1]
activate(x1) = [1 0] x1 + [0]
[0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ __(__(X, Y), Z) -> __(X, __(Y, Z))
, __(X, nil()) -> X
, __(nil(), X) -> X
, U11(tt()) -> U12(tt())}
Weak Trs:
{ isNePal(__(I, __(P, I))) -> U11(tt())
, activate(X) -> X
, U12(tt()) -> tt()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {U11(tt()) -> U12(tt())}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {2}, Uargs(U11) = {}, Uargs(U12) = {},
Uargs(isNePal) = {}, Uargs(activate) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 0] [0]
nil() = [0]
[0]
U11(x1) = [0 0] x1 + [1]
[0 0] [1]
tt() = [0]
[0]
U12(x1) = [0 0] x1 + [0]
[0 0] [1]
isNePal(x1) = [0 0] x1 + [1]
[0 0] [1]
activate(x1) = [1 0] x1 + [0]
[0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ __(__(X, Y), Z) -> __(X, __(Y, Z))
, __(X, nil()) -> X
, __(nil(), X) -> X}
Weak Trs:
{ U11(tt()) -> U12(tt())
, isNePal(__(I, __(P, I))) -> U11(tt())
, activate(X) -> X
, U12(tt()) -> tt()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {__(X, nil()) -> X}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {2}, Uargs(U11) = {}, Uargs(U12) = {},
Uargs(isNePal) = {}, Uargs(activate) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 0] [0]
nil() = [2]
[0]
U11(x1) = [0 0] x1 + [1]
[0 0] [1]
tt() = [0]
[0]
U12(x1) = [0 0] x1 + [1]
[0 0] [1]
isNePal(x1) = [0 0] x1 + [1]
[0 0] [1]
activate(x1) = [1 0] x1 + [0]
[0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ __(__(X, Y), Z) -> __(X, __(Y, Z))
, __(nil(), X) -> X}
Weak Trs:
{ __(X, nil()) -> X
, U11(tt()) -> U12(tt())
, isNePal(__(I, __(P, I))) -> U11(tt())
, activate(X) -> X
, U12(tt()) -> tt()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {__(nil(), X) -> X}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {2}, Uargs(U11) = {}, Uargs(U12) = {},
Uargs(isNePal) = {}, Uargs(activate) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[1 1] [0 1] [0]
nil() = [2]
[0]
U11(x1) = [1 0] x1 + [1]
[1 0] [1]
tt() = [0]
[0]
U12(x1) = [0 0] x1 + [1]
[0 0] [1]
isNePal(x1) = [0 0] x1 + [1]
[0 0] [1]
activate(x1) = [1 0] x1 + [0]
[0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {__(__(X, Y), Z) -> __(X, __(Y, Z))}
Weak Trs:
{ __(nil(), X) -> X
, __(X, nil()) -> X
, U11(tt()) -> U12(tt())
, isNePal(__(I, __(P, I))) -> U11(tt())
, activate(X) -> X
, U12(tt()) -> tt()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs: {__(__(X, Y), Z) -> __(X, __(Y, Z))}
Weak Trs:
{ __(nil(), X) -> X
, __(X, nil()) -> X
, U11(tt()) -> U12(tt())
, isNePal(__(I, __(P, I))) -> U11(tt())
, activate(X) -> X
, U12(tt()) -> tt()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The problem is match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ ___0(2, 2) -> 1
, nil_0() -> 1
, nil_0() -> 2
, U11_0(2) -> 1
, tt_0() -> 1
, tt_0() -> 2
, U12_0(2) -> 1
, isNePal_0(2) -> 1
, activate_0(2) -> 1}
Hurray, we answered YES(?,O(n^1))