We consider the following Problem: Strict Trs: { f(X, g(X)) -> f(1(), g(X)) , g(1()) -> g(0())} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: { f(X, g(X)) -> f(1(), g(X)) , g(1()) -> g(0())} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {g(1()) -> g(0())} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(f) = {}, Uargs(g) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: f(x1, x2) = [1 1] x1 + [0 0] x2 + [1] [0 0] [0 0] [0] g(x1) = [0 1] x1 + [0] [0 0] [1] 1() = [0] [2] 0() = [0] [1] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: {f(X, g(X)) -> f(1(), g(X))} Weak Trs: {g(1()) -> g(0())} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: {f(X, g(X)) -> f(1(), g(X))} Weak Trs: {g(1()) -> g(0())} 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: { f_0(2, 2) -> 1 , g_0(2) -> 1 , 1_0() -> 2 , 0_0() -> 2} Hurray, we answered YES(?,O(n^1))