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