We consider the following Problem: Strict Trs: { f(x, y) -> g1(x, x, y) , f(x, y) -> g1(y, x, x) , f(x, y) -> g2(x, y, y) , f(x, y) -> g2(y, y, x) , g1(x, x, y) -> h(x, y) , g1(y, x, x) -> h(x, y) , g2(x, y, y) -> h(x, y) , g2(y, y, x) -> h(x, y) , h(x, x) -> x} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: { f(x, y) -> g1(x, x, y) , f(x, y) -> g1(y, x, x) , f(x, y) -> g2(x, y, y) , f(x, y) -> g2(y, y, x) , g1(x, x, y) -> h(x, y) , g1(y, x, x) -> h(x, y) , g2(x, y, y) -> h(x, y) , g2(y, y, x) -> h(x, y) , h(x, x) -> x} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: { g2(x, y, y) -> h(x, y) , g2(y, y, x) -> h(x, y)} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(f) = {}, Uargs(g1) = {}, Uargs(g2) = {}, Uargs(h) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: f(x1, x2) = [1 1] x1 + [1 1] x2 + [0] [0 0] [0 0] [0] g1(x1, x2, x3) = [1 0] x1 + [0 1] x2 + [1 0] x3 + [0] [0 1] [1 0] [0 1] [0] g2(x1, x2, x3) = [1 1] x1 + [0 0] x2 + [1 1] x3 + [2] [0 0] [1 1] [0 0] [0] h(x1, x2) = [1 1] x1 + [0 0] x2 + [0] [0 0] [1 1] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { f(x, y) -> g1(x, x, y) , f(x, y) -> g1(y, x, x) , f(x, y) -> g2(x, y, y) , f(x, y) -> g2(y, y, x) , g1(x, x, y) -> h(x, y) , g1(y, x, x) -> h(x, y) , h(x, x) -> x} Weak Trs: { g2(x, y, y) -> h(x, y) , g2(y, y, x) -> h(x, y)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {h(x, x) -> x} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(f) = {}, Uargs(g1) = {}, Uargs(g2) = {}, Uargs(h) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: f(x1, x2) = [1 1] x1 + [1 1] x2 + [0] [0 0] [0 0] [0] g1(x1, x2, x3) = [1 1] x1 + [0 0] x2 + [1 1] x3 + [0] [0 0] [1 1] [0 0] [0] g2(x1, x2, x3) = [1 1] x1 + [0 0] x2 + [1 1] x3 + [2] [0 0] [1 1] [0 0] [0] h(x1, x2) = [1 1] x1 + [0 0] x2 + [2] [0 0] [1 1] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { f(x, y) -> g1(x, x, y) , f(x, y) -> g1(y, x, x) , f(x, y) -> g2(x, y, y) , f(x, y) -> g2(y, y, x) , g1(x, x, y) -> h(x, y) , g1(y, x, x) -> h(x, y)} Weak Trs: { h(x, x) -> x , g2(x, y, y) -> h(x, y) , g2(y, y, x) -> h(x, y)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: { g1(x, x, y) -> h(x, y) , g1(y, x, x) -> h(x, y)} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(f) = {}, Uargs(g1) = {}, Uargs(g2) = {}, Uargs(h) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: f(x1, x2) = [1 1] x1 + [1 1] x2 + [0] [0 0] [0 0] [0] g1(x1, x2, x3) = [1 0] x1 + [0 1] x2 + [1 0] x3 + [2] [0 1] [1 0] [0 1] [0] g2(x1, x2, x3) = [1 1] x1 + [0 0] x2 + [1 1] x3 + [0] [0 0] [1 1] [0 0] [0] h(x1, x2) = [1 1] x1 + [0 0] x2 + [0] [0 0] [0 1] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { f(x, y) -> g1(x, x, y) , f(x, y) -> g1(y, x, x) , f(x, y) -> g2(x, y, y) , f(x, y) -> g2(y, y, x)} Weak Trs: { g1(x, x, y) -> h(x, y) , g1(y, x, x) -> h(x, y) , h(x, x) -> x , g2(x, y, y) -> h(x, y) , g2(y, y, x) -> h(x, y)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: { f(x, y) -> g2(x, y, y) , f(x, y) -> g2(y, y, x)} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(f) = {}, Uargs(g1) = {}, Uargs(g2) = {}, Uargs(h) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: f(x1, x2) = [1 2] x1 + [1 0] x2 + [2] [0 0] [0 1] [0] g1(x1, x2, x3) = [1 0] x1 + [0 1] x2 + [1 0] x3 + [0] [0 1] [0 0] [0 1] [0] g2(x1, x2, x3) = [1 0] x1 + [0 0] x2 + [1 0] x3 + [0] [0 0] [0 1] [0 0] [0] h(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 1] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { f(x, y) -> g1(x, x, y) , f(x, y) -> g1(y, x, x)} Weak Trs: { f(x, y) -> g2(x, y, y) , f(x, y) -> g2(y, y, x) , g1(x, x, y) -> h(x, y) , g1(y, x, x) -> h(x, y) , h(x, x) -> x , g2(x, y, y) -> h(x, y) , g2(y, y, x) -> h(x, y)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: { f(x, y) -> g1(x, x, y) , f(x, y) -> g1(y, x, x)} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(f) = {}, Uargs(g1) = {}, Uargs(g2) = {}, Uargs(h) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: f(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [1 1] [1 1] [0] g1(x1, x2, x3) = [1 0] x1 + [0 0] x2 + [1 0] x3 + [0] [0 1] [0 0] [1 1] [0] g2(x1, x2, x3) = [1 0] x1 + [0 0] x2 + [1 0] x3 + [0] [1 1] [0 0] [0 1] [0] h(x1, x2) = [0 0] x1 + [1 0] x2 + [0] [0 0] [0 1] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Weak Trs: { f(x, y) -> g1(x, x, y) , f(x, y) -> g1(y, x, x) , f(x, y) -> g2(x, y, y) , f(x, y) -> g2(y, y, x) , g1(x, x, y) -> h(x, y) , g1(y, x, x) -> h(x, y) , h(x, x) -> x , g2(x, y, y) -> h(x, y) , g2(y, y, x) -> h(x, y)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { f(x, y) -> g1(x, x, y) , f(x, y) -> g1(y, x, x) , f(x, y) -> g2(x, y, y) , f(x, y) -> g2(y, y, x) , g1(x, x, y) -> h(x, y) , g1(y, x, x) -> h(x, y) , h(x, x) -> x , g2(x, y, y) -> h(x, y) , g2(y, y, x) -> h(x, y)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: Empty rules are trivially bounded Hurray, we answered YES(?,O(n^1))