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