We consider the following Problem: Strict Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , quot(x, s(y)) -> if_quot(le(s(y), x), x, s(y)) , if_quot(true(), x, y) -> s(quot(minus(x, y), y)) , if_quot(false(), x, y) -> 0()} 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)) -> minus(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , quot(x, s(y)) -> if_quot(le(s(y), x), x, s(y)) , if_quot(true(), x, y) -> s(quot(minus(x, y), y)) , if_quot(false(), x, 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: { le(0(), y) -> true() , le(s(x), 0()) -> false()} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(minus) = {}, Uargs(s) = {1}, Uargs(le) = {}, Uargs(quot) = {1}, Uargs(if_quot) = {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] [0 0] [0 0] [1] 0() = [0] [0] s(x1) = [1 0] x1 + [0] [0 0] [1] le(x1, x2) = [0 0] x1 + [0 0] x2 + [1] [0 0] [0 0] [1] true() = [0] [0] false() = [0] [0] quot(x1, x2) = [1 2] x1 + [0 0] x2 + [1] [0 0] [0 0] [1] if_quot(x1, x2, x3) = [1 0] x1 + [1 1] x2 + [0 0] x3 + [0] [0 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 , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , quot(x, s(y)) -> if_quot(le(s(y), x), x, s(y)) , if_quot(true(), x, y) -> s(quot(minus(x, y), y)) , if_quot(false(), x, y) -> 0()} Weak Trs: { le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {if_quot(false(), x, y) -> 0()} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(minus) = {}, Uargs(s) = {1}, Uargs(le) = {}, Uargs(quot) = {1}, Uargs(if_quot) = {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] [0 0] [0 0] [1] 0() = [0] [0] s(x1) = [1 0] x1 + [0] [0 0] [1] le(x1, x2) = [0 0] x1 + [0 0] x2 + [1] [0 0] [0 0] [1] true() = [0] [0] false() = [1] [0] quot(x1, x2) = [1 2] x1 + [0 0] x2 + [1] [0 0] [0 0] [1] if_quot(x1, x2, x3) = [1 0] x1 + [1 1] x2 + [0 0] x3 + [0] [0 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 , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , quot(x, s(y)) -> if_quot(le(s(y), x), x, s(y)) , if_quot(true(), x, y) -> s(quot(minus(x, y), y))} Weak Trs: { if_quot(false(), x, y) -> 0() , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {if_quot(true(), x, y) -> s(quot(minus(x, y), y))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(minus) = {}, Uargs(s) = {1}, Uargs(le) = {}, Uargs(quot) = {1}, Uargs(if_quot) = {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] [0 0] [0 0] [1] 0() = [0] [0] s(x1) = [1 0] x1 + [0] [0 0] [1] le(x1, x2) = [0 0] x1 + [0 0] x2 + [1] [0 0] [0 0] [1] true() = [1] [1] false() = [0] [0] quot(x1, x2) = [1 2] x1 + [0 0] x2 + [1] [0 0] [0 0] [1] if_quot(x1, x2, x3) = [1 3] x1 + [1 1] x2 + [0 1] x3 + [2] [0 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 , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , quot(x, s(y)) -> if_quot(le(s(y), x), x, s(y))} Weak Trs: { if_quot(true(), x, y) -> s(quot(minus(x, y), y)) , if_quot(false(), x, y) -> 0() , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {le(s(x), s(y)) -> le(x, y)} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(minus) = {}, Uargs(s) = {1}, Uargs(le) = {}, Uargs(quot) = {1}, Uargs(if_quot) = {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 0] [0 0] [0] 0() = [0] [0] s(x1) = [1 0] x1 + [0] [0 1] [2] le(x1, x2) = [0 0] x1 + [0 1] x2 + [0] [0 0] [0 0] [3] true() = [0] [2] false() = [0] [2] quot(x1, x2) = [1 1] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] if_quot(x1, x2, x3) = [1 2] x1 + [1 0] x2 + [0 0] x3 + [0] [0 0] [0 1] [0 0] [3] 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)) -> minus(x, y) , quot(x, s(y)) -> if_quot(le(s(y), x), x, s(y))} Weak Trs: { le(s(x), s(y)) -> le(x, y) , if_quot(true(), x, y) -> s(quot(minus(x, y), y)) , if_quot(false(), x, y) -> 0() , le(0(), y) -> true() , le(s(x), 0()) -> false()} 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)) -> minus(x, y)} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(minus) = {}, Uargs(s) = {1}, Uargs(le) = {}, Uargs(quot) = {1}, Uargs(if_quot) = {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] [0 0] [0 0] [1] 0() = [0] [0] s(x1) = [1 0] x1 + [1] [0 0] [0] le(x1, x2) = [0 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [3] true() = [0] [3] false() = [0] [0] quot(x1, x2) = [1 1] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] if_quot(x1, x2, x3) = [1 1] x1 + [1 1] x2 + [0 0] x3 + [0] [0 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 , quot(x, s(y)) -> if_quot(le(s(y), x), x, s(y))} Weak Trs: { minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , if_quot(true(), x, y) -> s(quot(minus(x, y), y)) , if_quot(false(), x, y) -> 0() , le(0(), y) -> true() , le(s(x), 0()) -> false()} 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(le) = {}, Uargs(quot) = {1}, Uargs(if_quot) = {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] [0 1] [0 0] [0] 0() = [0] [1] s(x1) = [1 0] x1 + [0] [0 1] [0] le(x1, x2) = [0 0] x1 + [0 0] x2 + [1] [0 1] [0 0] [3] true() = [1] [0] false() = [0] [0] quot(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [0] if_quot(x1, x2, x3) = [1 0] x1 + [1 0] x2 + [0 0] x3 + [0] [0 0] [0 0] [0 0] [1] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: {quot(x, s(y)) -> if_quot(le(s(y), x), x, s(y))} Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , if_quot(true(), x, y) -> s(quot(minus(x, y), y)) , if_quot(false(), x, y) -> 0() , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: {quot(x, s(y)) -> if_quot(le(s(y), x), x, s(y))} Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , if_quot(true(), x, y) -> s(quot(minus(x, y), y)) , if_quot(false(), x, y) -> 0() , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We have computed the following dependency pairs Strict DPs: {quot^#(x, s(y)) -> if_quot^#(le(s(y), x), x, s(y))} Weak DPs: { minus^#(x, 0()) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , le^#(s(x), s(y)) -> le^#(x, y) , if_quot^#(true(), x, y) -> quot^#(minus(x, y), y) , if_quot^#(false(), x, y) -> c_6() , le^#(0(), y) -> c_7() , le^#(s(x), 0()) -> c_8()} We consider the following Problem: Strict DPs: {quot^#(x, s(y)) -> if_quot^#(le(s(y), x), x, s(y))} Strict Trs: {quot(x, s(y)) -> if_quot(le(s(y), x), x, s(y))} Weak DPs: { minus^#(x, 0()) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , le^#(s(x), s(y)) -> le^#(x, y) , if_quot^#(true(), x, y) -> quot^#(minus(x, y), y) , if_quot^#(false(), x, y) -> c_6() , le^#(0(), y) -> c_7() , le^#(s(x), 0()) -> c_8()} Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , if_quot(true(), x, y) -> s(quot(minus(x, y), y)) , if_quot(false(), x, y) -> 0() , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We replace strict/weak-rules by the corresponding usable rules: Weak Usable Rules: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} We consider the following Problem: Strict DPs: {quot^#(x, s(y)) -> if_quot^#(le(s(y), x), x, s(y))} Weak DPs: { minus^#(x, 0()) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , le^#(s(x), s(y)) -> le^#(x, y) , if_quot^#(true(), x, y) -> quot^#(minus(x, y), y) , if_quot^#(false(), x, y) -> c_6() , le^#(0(), y) -> c_7() , le^#(s(x), 0()) -> c_8()} Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict DPs: {quot^#(x, s(y)) -> if_quot^#(le(s(y), x), x, s(y))} Weak DPs: { minus^#(x, 0()) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , le^#(s(x), s(y)) -> le^#(x, y) , if_quot^#(true(), x, y) -> quot^#(minus(x, y), y) , if_quot^#(false(), x, y) -> c_6() , le^#(0(), y) -> c_7() , le^#(s(x), 0()) -> c_8()} Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We use following congruence DG for path analysis ->6:{1,5} [ YES(O(1),O(1)) ] | `->7:{6} [ YES(O(1),O(1)) ] ->4:{3} [ subsumed ] | `->5:{2} [ YES(O(1),O(1)) ] ->1:{4} [ subsumed ] | |->2:{7} [ YES(O(1),O(1)) ] | `->3:{8} [ YES(O(1),O(1)) ] Here dependency-pairs are as follows: Strict DPs: {1: quot^#(x, s(y)) -> if_quot^#(le(s(y), x), x, s(y))} WeakDPs DPs: { 2: minus^#(x, 0()) -> c_2() , 3: minus^#(s(x), s(y)) -> minus^#(x, y) , 4: le^#(s(x), s(y)) -> le^#(x, y) , 5: if_quot^#(true(), x, y) -> quot^#(minus(x, y), y) , 6: if_quot^#(false(), x, y) -> c_6() , 7: le^#(0(), y) -> c_7() , 8: le^#(s(x), 0()) -> c_8()} * Path 6:{1,5}: YES(O(1),O(1)) ---------------------------- We consider the following Problem: Strict DPs: {quot^#(x, s(y)) -> if_quot^#(le(s(y), x), x, s(y))} Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: quot^#(x, s(y)) -> if_quot^#(le(s(y), x), x, s(y)) together with the congruence-graph ->1:{1} Noncyclic, trivial, SCC Here dependency-pairs are as follows: Strict DPs: {1: quot^#(x, s(y)) -> if_quot^#(le(s(y), x), x, s(y))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: {1: quot^#(x, s(y)) -> if_quot^#(le(s(y), x), x, s(y))} We consider the following Problem: Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} 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 6:{1,5}->7:{6}: YES(O(1),O(1)) ----------------------------------- We consider the following Problem: Weak DPs: { if_quot^#(true(), x, y) -> quot^#(minus(x, y), y) , quot^#(x, s(y)) -> if_quot^#(le(s(y), x), x, s(y))} Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: if_quot^#(true(), x, y) -> quot^#(minus(x, y), y) -->_1 quot^#(x, s(y)) -> if_quot^#(le(s(y), x), x, s(y)) :2 2: quot^#(x, s(y)) -> if_quot^#(le(s(y), x), x, s(y)) -->_1 if_quot^#(true(), x, y) -> quot^#(minus(x, y), y) :1 together with the congruence-graph ->1:{1,2} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: { 1: if_quot^#(true(), x, y) -> quot^#(minus(x, y), y) , 2: quot^#(x, s(y)) -> if_quot^#(le(s(y), x), x, s(y))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: { 1: if_quot^#(true(), x, y) -> quot^#(minus(x, y), y) , 2: quot^#(x, s(y)) -> if_quot^#(le(s(y), x), x, s(y))} We consider the following Problem: Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} 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 4:{3}: subsumed -------------------- This path is subsumed by the proof of paths 4:{3}->5:{2}. * Path 4:{3}->5:{2}: YES(O(1),O(1)) --------------------------------- We consider the following Problem: Weak DPs: {minus^#(s(x), s(y)) -> minus^#(x, y)} Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: minus^#(s(x), s(y)) -> minus^#(x, y) -->_1 minus^#(s(x), s(y)) -> minus^#(x, y) :1 together with the congruence-graph ->1:{1} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: {1: minus^#(s(x), s(y)) -> 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)) -> minus^#(x, y)} We consider the following Problem: Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} 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:{8}, 1:{4}->2:{7}. * Path 1:{4}->2:{7}: YES(O(1),O(1)) --------------------------------- We consider the following Problem: Weak DPs: {le^#(s(x), s(y)) -> le^#(x, y)} Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: le^#(s(x), s(y)) -> le^#(x, y) -->_1 le^#(s(x), s(y)) -> le^#(x, y) :1 together with the congruence-graph ->1:{1} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: {1: le^#(s(x), s(y)) -> le^#(x, y)} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: {1: le^#(s(x), s(y)) -> le^#(x, y)} We consider the following Problem: Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} 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}->3:{8}: YES(O(1),O(1)) --------------------------------- We consider the following Problem: Weak DPs: {le^#(s(x), s(y)) -> le^#(x, y)} Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: le^#(s(x), s(y)) -> le^#(x, y) -->_1 le^#(s(x), s(y)) -> le^#(x, y) :1 together with the congruence-graph ->1:{1} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: {1: le^#(s(x), s(y)) -> le^#(x, y)} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: {1: le^#(s(x), s(y)) -> le^#(x, y)} We consider the following Problem: Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , le(s(x), s(y)) -> le(x, y) , le(0(), y) -> true() , le(s(x), 0()) -> false()} 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))