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