We consider the following Problem: Strict Trs: { q(x, 0(), s(z)) -> s(q(x, s(z), s(z))) , q(s(x), s(y), z) -> q(x, y, z) , q(0(), s(y), s(z)) -> 0()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: { q(x, 0(), s(z)) -> s(q(x, s(z), s(z))) , q(s(x), s(y), z) -> q(x, y, z) , q(0(), s(y), s(z)) -> 0()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {q(0(), s(y), s(z)) -> 0()} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(s) = {1}, Uargs(q) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: 0() = [0] [0] s(x1) = [1 2] x1 + [0] [0 0] [1] q(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1] [0 0] [0 0] [0 0] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { q(x, 0(), s(z)) -> s(q(x, s(z), s(z))) , q(s(x), s(y), z) -> q(x, y, z)} Weak Trs: {q(0(), s(y), s(z)) -> 0()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {q(s(x), s(y), z) -> q(x, y, z)} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(s) = {1}, Uargs(q) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: 0() = [0] [0] s(x1) = [1 3] x1 + [0] [0 0] [1] q(x1, x2, x3) = [1 1] x1 + [0 0] x2 + [0 0] x3 + [0] [0 0] [0 0] [0 1] [3] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: {q(x, 0(), s(z)) -> s(q(x, s(z), s(z)))} Weak Trs: { q(s(x), s(y), z) -> q(x, y, z) , q(0(), s(y), s(z)) -> 0()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: {q(x, 0(), s(z)) -> s(q(x, s(z), s(z)))} Weak Trs: { q(s(x), s(y), z) -> q(x, y, z) , q(0(), s(y), s(z)) -> 0()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We have computed the following dependency pairs Strict DPs: {q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z))} Weak DPs: { q^#(s(x), s(y), z) -> q^#(x, y, z) , q^#(0(), s(y), s(z)) -> c_3()} We consider the following Problem: Strict DPs: {q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z))} Strict Trs: {q(x, 0(), s(z)) -> s(q(x, s(z), s(z)))} Weak DPs: { q^#(s(x), s(y), z) -> q^#(x, y, z) , q^#(0(), s(y), s(z)) -> c_3()} Weak Trs: { q(s(x), s(y), z) -> q(x, y, z) , q(0(), s(y), s(z)) -> 0()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: No rule is usable. We consider the following Problem: Strict DPs: {q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z))} Weak DPs: { q^#(s(x), s(y), z) -> q^#(x, y, z) , q^#(0(), s(y), s(z)) -> c_3()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict DPs: {q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z))} Weak DPs: { q^#(s(x), s(y), z) -> q^#(x, y, z) , q^#(0(), s(y), s(z)) -> c_3()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We use following congruence DG for path analysis ->1:{1,2} [ YES(O(1),O(1)) ] | `->2:{3} [ YES(O(1),O(1)) ] Here dependency-pairs are as follows: Strict DPs: {1: q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z))} WeakDPs DPs: { 2: q^#(s(x), s(y), z) -> q^#(x, y, z) , 3: q^#(0(), s(y), s(z)) -> c_3()} * Path 1:{1,2}: YES(O(1),O(1)) ---------------------------- We consider the following Problem: Strict DPs: {q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z))} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z)) together with the congruence-graph ->1:{1} Noncyclic, trivial, SCC Here dependency-pairs are as follows: Strict DPs: {1: q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: {1: q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z))} We consider the following Problem: StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: Empty rules are trivially bounded * Path 1:{1,2}->2:{3}: YES(O(1),O(1)) ----------------------------------- We consider the following Problem: Weak DPs: { q^#(s(x), s(y), z) -> q^#(x, y, z) , q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z))} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: q^#(s(x), s(y), z) -> q^#(x, y, z) -->_1 q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z)) :2 -->_1 q^#(s(x), s(y), z) -> q^#(x, y, z) :1 2: q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z)) -->_1 q^#(s(x), s(y), z) -> q^#(x, y, z) :1 together with the congruence-graph ->1:{1,2} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: { 1: q^#(s(x), s(y), z) -> q^#(x, y, z) , 2: q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: { 1: q^#(s(x), s(y), z) -> q^#(x, y, z) , 2: q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z))} We consider the following Problem: StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: Empty rules are trivially bounded * Path 1:{1,2}->2:{3}: YES(O(1),O(1)) ----------------------------------- We consider the following Problem: Weak DPs: { q^#(s(x), s(y), z) -> q^#(x, y, z) , q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z))} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: q^#(s(x), s(y), z) -> q^#(x, y, z) -->_1 q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z)) :2 -->_1 q^#(s(x), s(y), z) -> q^#(x, y, z) :1 2: q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z)) -->_1 q^#(s(x), s(y), z) -> q^#(x, y, z) :1 together with the congruence-graph ->1:{1,2} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: { 1: q^#(s(x), s(y), z) -> q^#(x, y, z) , 2: q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: { 1: q^#(s(x), s(y), z) -> q^#(x, y, z) , 2: q^#(x, 0(), s(z)) -> q^#(x, s(z), s(z))} We consider the following Problem: StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: Empty rules are trivially bounded Hurray, we answered YES(?,O(n^1))