We consider the following Problem:
Strict Trs:
{ f(0(), y) -> y
, f(x, 0()) -> x
, f(i(x), y) -> i(x)
, f(f(x, y), z) -> f(x, f(y, z))
, f(g(x, y), z) -> g(f(x, z), f(y, z))
, f(1(), g(x, y)) -> x
, f(2(), g(x, y)) -> y}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
We consider the following Problem:
Strict Trs:
{ f(0(), y) -> y
, f(x, 0()) -> x
, f(i(x), y) -> i(x)
, f(f(x, y), z) -> f(x, f(y, z))
, f(g(x, y), z) -> g(f(x, z), f(y, z))
, f(1(), g(x, y)) -> x
, f(2(), g(x, y)) -> y}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
We consider the following Problem:
Strict Trs:
{ f(0(), y) -> y
, f(x, 0()) -> x
, f(i(x), y) -> i(x)
, f(f(x, y), z) -> f(x, f(y, z))
, f(g(x, y), z) -> g(f(x, z), f(y, z))
, f(1(), g(x, y)) -> x
, f(2(), g(x, y)) -> y}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The following argument positions are usable:
Uargs(f) = {2}, Uargs(i) = {}, Uargs(g) = {1, 2}
We have the following restricted polynomial interpretation:
Interpretation Functions:
[f](x1, x2) = 2 + 2*x1 + x1*x2 + x2
[0]() = 0
[i](x1) = 2
[g](x1, x2) = 3 + x1 + x2
[1]() = 0
[2]() = 0
Hurray, we answered YES(?,O(n^2))