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))