We consider the following Problem: Strict Trs: { minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y)) , p(s(X)) -> X , div(0(), s(Y)) -> 0() , div(s(X), s(Y)) -> s(div(minus(X, Y), s(Y)))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: { minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y)) , p(s(X)) -> X , div(0(), s(Y)) -> 0() , div(s(X), s(Y)) -> s(div(minus(X, Y), s(Y)))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {div(0(), s(Y)) -> 0()} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(minus) = {}, Uargs(s) = {1}, Uargs(p) = {1}, Uargs(div) = {1} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: minus(x1, x2) = [1 0] x1 + [0 0] x2 + [1] [1 0] [0 0] [1] 0() = [0] [0] s(x1) = [1 0] x1 + [0] [0 0] [1] p(x1) = [1 0] x1 + [0] [0 0] [1] div(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: { minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y)) , p(s(X)) -> X , div(s(X), s(Y)) -> s(div(minus(X, Y), s(Y)))} Weak Trs: {div(0(), s(Y)) -> 0()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {minus(s(X), s(Y)) -> p(minus(X, Y))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(minus) = {}, Uargs(s) = {1}, Uargs(p) = {1}, Uargs(div) = {1} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: minus(x1, x2) = [1 0] x1 + [0 0] x2 + [1] [1 0] [0 0] [1] 0() = [0] [0] s(x1) = [1 0] x1 + [2] [0 0] [1] p(x1) = [1 0] x1 + [0] [0 0] [1] div(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { minus(X, 0()) -> X , p(s(X)) -> X , div(s(X), s(Y)) -> s(div(minus(X, Y), s(Y)))} Weak Trs: { minus(s(X), s(Y)) -> p(minus(X, Y)) , div(0(), s(Y)) -> 0()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {minus(X, 0()) -> X} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(minus) = {}, Uargs(s) = {1}, Uargs(p) = {1}, Uargs(div) = {1} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: minus(x1, x2) = [1 0] x1 + [0 0] x2 + [1] [1 1] [0 0] [1] 0() = [0] [0] s(x1) = [1 0] x1 + [0] [0 0] [1] p(x1) = [1 0] x1 + [0] [1 0] [1] div(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { p(s(X)) -> X , div(s(X), s(Y)) -> s(div(minus(X, Y), s(Y)))} Weak Trs: { minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y)) , div(0(), s(Y)) -> 0()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {p(s(X)) -> X} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(minus) = {}, Uargs(s) = {1}, Uargs(p) = {1}, Uargs(div) = {1} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: minus(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 1] [0 0] [1] 0() = [0] [0] s(x1) = [1 0] x1 + [1] [0 1] [0] p(x1) = [1 0] x1 + [1] [0 1] [0] div(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [1 0] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: {div(s(X), s(Y)) -> s(div(minus(X, Y), s(Y)))} Weak Trs: { p(s(X)) -> X , minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y)) , div(0(), s(Y)) -> 0()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: {div(s(X), s(Y)) -> s(div(minus(X, Y), s(Y)))} Weak Trs: { p(s(X)) -> X , minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y)) , div(0(), s(Y)) -> 0()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We have computed the following dependency pairs Strict DPs: {div^#(s(X), s(Y)) -> div^#(minus(X, Y), s(Y))} Weak DPs: { p^#(s(X)) -> c_2() , minus^#(X, 0()) -> c_3() , minus^#(s(X), s(Y)) -> p^#(minus(X, Y)) , div^#(0(), s(Y)) -> c_5()} We consider the following Problem: Strict DPs: {div^#(s(X), s(Y)) -> div^#(minus(X, Y), s(Y))} Strict Trs: {div(s(X), s(Y)) -> s(div(minus(X, Y), s(Y)))} Weak DPs: { p^#(s(X)) -> c_2() , minus^#(X, 0()) -> c_3() , minus^#(s(X), s(Y)) -> p^#(minus(X, Y)) , div^#(0(), s(Y)) -> c_5()} Weak Trs: { p(s(X)) -> X , minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y)) , div(0(), s(Y)) -> 0()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We replace strict/weak-rules by the corresponding usable rules: Weak Usable Rules: { p(s(X)) -> X , minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y))} We consider the following Problem: Strict DPs: {div^#(s(X), s(Y)) -> div^#(minus(X, Y), s(Y))} Weak DPs: { p^#(s(X)) -> c_2() , minus^#(X, 0()) -> c_3() , minus^#(s(X), s(Y)) -> p^#(minus(X, Y)) , div^#(0(), s(Y)) -> c_5()} Weak Trs: { p(s(X)) -> X , minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: Dependency Pairs: {div^#(s(X), s(Y)) -> div^#(minus(X, Y), s(Y))} Interpretation of constant growth: ---------------------------------- The following argument positions are usable: Uargs(minus) = {}, Uargs(s) = {}, Uargs(p) = {1}, Uargs(div) = {}, Uargs(div^#) = {1}, Uargs(p^#) = {1}, Uargs(minus^#) = {} We have the following constructor-based EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: minus(x1, x2) = [1 0] x1 + [0 0] x2 + [1] [0 1] [1 0] [1] 0() = [0] [0] s(x1) = [1 0] x1 + [2] [0 1] [0] p(x1) = [1 0] x1 + [1] [0 1] [1] div(x1, x2) = [0 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [0] div^#(x1, x2) = [1 0] x1 + [0 0] x2 + [1] [0 0] [0 0] [1] p^#(x1) = [1 0] x1 + [1] [0 0] [1] c_2() = [0] [0] minus^#(x1, x2) = [1 0] x1 + [1 0] x2 + [1] [0 0] [0 0] [1] c_3() = [0] [0] c_5() = [0] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Weak DPs: { div^#(s(X), s(Y)) -> div^#(minus(X, Y), s(Y)) , p^#(s(X)) -> c_2() , minus^#(X, 0()) -> c_3() , minus^#(s(X), s(Y)) -> p^#(minus(X, Y)) , div^#(0(), s(Y)) -> c_5()} Weak Trs: { p(s(X)) -> X , minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We use following congruence DG for path analysis ->4:{1} [ subsumed ] | `->5:{5} [ YES(O(1),O(1)) ] ->2:{3} [ YES(O(1),O(1)) ] ->1:{4} [ subsumed ] | `->3:{2} [ YES(O(1),O(1)) ] Here dependency-pairs are as follows: WeakDPs DPs: { 1: div^#(s(X), s(Y)) -> div^#(minus(X, Y), s(Y)) , 2: p^#(s(X)) -> c_2() , 3: minus^#(X, 0()) -> c_3() , 4: minus^#(s(X), s(Y)) -> p^#(minus(X, Y)) , 5: div^#(0(), s(Y)) -> c_5()} * Path 4:{1}: subsumed -------------------- This path is subsumed by the proof of paths 4:{1}->5:{5}. * Path 4:{1}->5:{5}: YES(O(1),O(1)) --------------------------------- We consider the following Problem: Weak DPs: {div^#(s(X), s(Y)) -> div^#(minus(X, Y), s(Y))} Weak Trs: { p(s(X)) -> X , minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y))} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: div^#(s(X), s(Y)) -> div^#(minus(X, Y), s(Y)) -->_1 div^#(s(X), s(Y)) -> div^#(minus(X, Y), s(Y)) :1 together with the congruence-graph ->1:{1} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: {1: div^#(s(X), s(Y)) -> div^#(minus(X, Y), s(Y))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: {1: div^#(s(X), s(Y)) -> div^#(minus(X, Y), s(Y))} We consider the following Problem: Weak Trs: { p(s(X)) -> X , minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y))} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { p(s(X)) -> X , minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y))} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: No rule is usable. We consider the following Problem: StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: Empty rules are trivially bounded * Path 2:{3}: YES(O(1),O(1)) -------------------------- We consider the following Problem: Weak Trs: { p(s(X)) -> X , minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y))} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { p(s(X)) -> X , minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y))} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { p(s(X)) -> X , minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y))} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: No rule is usable. We consider the following Problem: StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: Empty rules are trivially bounded * Path 1:{4}: subsumed -------------------- This path is subsumed by the proof of paths 1:{4}->3:{2}. * Path 1:{4}->3:{2}: YES(O(1),O(1)) --------------------------------- We consider the following Problem: Weak DPs: {minus^#(s(X), s(Y)) -> p^#(minus(X, Y))} Weak Trs: { p(s(X)) -> X , minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y))} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: minus^#(s(X), s(Y)) -> p^#(minus(X, Y)) together with the congruence-graph ->1:{1} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: {1: minus^#(s(X), s(Y)) -> p^#(minus(X, Y))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: {1: minus^#(s(X), s(Y)) -> p^#(minus(X, Y))} We consider the following Problem: Weak Trs: { p(s(X)) -> X , minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y))} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { p(s(X)) -> X , minus(X, 0()) -> X , minus(s(X), s(Y)) -> p(minus(X, Y))} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: No rule is usable. 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))