We consider the following Problem:
Strict Trs:
{ g(c(), g(c(), x)) -> g(e(), g(d(), x))
, g(d(), g(d(), x)) -> g(c(), g(e(), x))
, g(e(), g(e(), x)) -> g(d(), g(c(), x))
, f(g(x, y)) -> g(y, g(f(f(x)), a()))
, g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b())))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ g(c(), g(c(), x)) -> g(e(), g(d(), x))
, g(d(), g(d(), x)) -> g(c(), g(e(), x))
, g(e(), g(e(), x)) -> g(d(), g(c(), x))
, f(g(x, y)) -> g(y, g(f(f(x)), a()))
, g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b())))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {g(e(), g(e(), x)) -> g(d(), g(c(), x))}
Interpretation of nonconstant growth:
-------------------------------------
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
g(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 1] [0]
c() = [0]
[0]
e() = [2]
[0]
d() = [1]
[0]
f(x1) = [1 0] x1 + [0]
[0 0] [1]
a() = [1]
[0]
b() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ g(c(), g(c(), x)) -> g(e(), g(d(), x))
, g(d(), g(d(), x)) -> g(c(), g(e(), x))
, f(g(x, y)) -> g(y, g(f(f(x)), a()))
, g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b())))}
Weak Trs: {g(e(), g(e(), x)) -> g(d(), g(c(), x))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {g(d(), g(d(), x)) -> g(c(), g(e(), x))}
Interpretation of nonconstant growth:
-------------------------------------
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
g(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[1 0] [0 1] [2]
c() = [0]
[0]
e() = [1]
[0]
d() = [1]
[0]
f(x1) = [1 0] x1 + [0]
[0 0] [1]
a() = [1]
[0]
b() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ g(c(), g(c(), x)) -> g(e(), g(d(), x))
, f(g(x, y)) -> g(y, g(f(f(x)), a()))
, g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b())))}
Weak Trs:
{ g(d(), g(d(), x)) -> g(c(), g(e(), x))
, g(e(), g(e(), x)) -> g(d(), g(c(), x))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ g(c(), g(c(), x)) -> g(e(), g(d(), x))
, f(g(x, y)) -> g(y, g(f(f(x)), a()))
, g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b())))}
Weak Trs:
{ g(d(), g(d(), x)) -> g(c(), g(e(), x))
, g(e(), g(e(), x)) -> g(d(), g(c(), x))}
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:
{ g_0(2, 2) -> 1
, c_0() -> 2
, e_0() -> 2
, d_0() -> 2
, f_0(2) -> 1
, a_0() -> 2
, b_0() -> 2}
Hurray, we answered YES(?,O(n^1))