We consider the following Problem:
Strict Trs:
{ d(x) -> e(u(x))
, d(u(x)) -> c(x)
, c(u(x)) -> b(x)
, v(e(x)) -> x
, b(u(x)) -> a(e(x))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ d(x) -> e(u(x))
, d(u(x)) -> c(x)
, c(u(x)) -> b(x)
, v(e(x)) -> x
, b(u(x)) -> a(e(x))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {b(u(x)) -> a(e(x))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(d) = {}, Uargs(e) = {}, Uargs(u) = {}, Uargs(c) = {},
Uargs(b) = {}, Uargs(v) = {}, Uargs(a) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
d(x1) = [0 0] x1 + [1]
[0 0] [1]
e(x1) = [0 0] x1 + [1]
[1 0] [1]
u(x1) = [0 0] x1 + [0]
[0 0] [0]
c(x1) = [0 0] x1 + [1]
[0 0] [1]
b(x1) = [0 0] x1 + [1]
[0 0] [1]
v(x1) = [0 1] x1 + [0]
[0 0] [1]
a(x1) = [0 0] x1 + [0]
[0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ d(x) -> e(u(x))
, d(u(x)) -> c(x)
, c(u(x)) -> b(x)
, v(e(x)) -> x}
Weak Trs: {b(u(x)) -> a(e(x))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {c(u(x)) -> b(x)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(d) = {}, Uargs(e) = {}, Uargs(u) = {}, Uargs(c) = {},
Uargs(b) = {}, Uargs(v) = {}, Uargs(a) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
d(x1) = [0 0] x1 + [1]
[0 0] [1]
e(x1) = [0 0] x1 + [1]
[1 0] [1]
u(x1) = [0 0] x1 + [0]
[0 0] [0]
c(x1) = [0 0] x1 + [1]
[0 0] [1]
b(x1) = [0 0] x1 + [0]
[0 0] [1]
v(x1) = [0 1] x1 + [0]
[0 0] [1]
a(x1) = [0 0] x1 + [0]
[0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ d(x) -> e(u(x))
, d(u(x)) -> c(x)
, v(e(x)) -> x}
Weak Trs:
{ c(u(x)) -> b(x)
, b(u(x)) -> a(e(x))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {d(u(x)) -> c(x)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(d) = {}, Uargs(e) = {}, Uargs(u) = {}, Uargs(c) = {},
Uargs(b) = {}, Uargs(v) = {}, Uargs(a) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
d(x1) = [0 0] x1 + [1]
[0 0] [1]
e(x1) = [0 0] x1 + [1]
[1 0] [1]
u(x1) = [0 0] x1 + [0]
[0 0] [0]
c(x1) = [0 0] x1 + [0]
[0 0] [1]
b(x1) = [0 0] x1 + [0]
[0 0] [1]
v(x1) = [0 1] x1 + [0]
[0 0] [1]
a(x1) = [0 0] x1 + [0]
[0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ d(x) -> e(u(x))
, v(e(x)) -> x}
Weak Trs:
{ d(u(x)) -> c(x)
, c(u(x)) -> b(x)
, b(u(x)) -> a(e(x))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {d(x) -> e(u(x))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(d) = {}, Uargs(e) = {}, Uargs(u) = {}, Uargs(c) = {},
Uargs(b) = {}, Uargs(v) = {}, Uargs(a) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
d(x1) = [0 0] x1 + [3]
[0 0] [1]
e(x1) = [0 0] x1 + [1]
[1 0] [1]
u(x1) = [0 0] x1 + [0]
[0 0] [0]
c(x1) = [0 0] x1 + [1]
[0 0] [1]
b(x1) = [0 0] x1 + [1]
[0 0] [1]
v(x1) = [0 1] x1 + [0]
[0 0] [1]
a(x1) = [0 0] x1 + [1]
[0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {v(e(x)) -> x}
Weak Trs:
{ d(x) -> e(u(x))
, d(u(x)) -> c(x)
, c(u(x)) -> b(x)
, b(u(x)) -> a(e(x))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {v(e(x)) -> x}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(d) = {}, Uargs(e) = {}, Uargs(u) = {}, Uargs(c) = {},
Uargs(b) = {}, Uargs(v) = {}, Uargs(a) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
d(x1) = [1 0] x1 + [1]
[0 1] [1]
e(x1) = [1 0] x1 + [0]
[0 1] [0]
u(x1) = [0 0] x1 + [0]
[0 0] [0]
c(x1) = [0 0] x1 + [1]
[0 0] [1]
b(x1) = [0 0] x1 + [1]
[0 0] [1]
v(x1) = [1 0] x1 + [1]
[0 1] [1]
a(x1) = [0 0] x1 + [1]
[0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Weak Trs:
{ v(e(x)) -> x
, d(x) -> e(u(x))
, d(u(x)) -> c(x)
, c(u(x)) -> b(x)
, b(u(x)) -> a(e(x))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ v(e(x)) -> x
, d(x) -> e(u(x))
, d(u(x)) -> c(x)
, c(u(x)) -> b(x)
, b(u(x)) -> a(e(x))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))