We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ f(x, x, y) -> x
, f(x, y, y) -> y
, f(x, y, g(y)) -> x
, f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v))
, f(g(x), x, y) -> y }
Obligation:
runtime complexity
Answer:
YES(?,O(n^1))
The problem is match-bounded by 0. The enriched problem is
compatible with the following automaton.
{ f_0(2, 2, 2) -> 1
, g_0(2) -> 1
, g_0(2) -> 2 }
Hurray, we answered YES(?,O(n^1))