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