We consider the following Problem: Strict Trs: { U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X)) , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , and(tt(), X) -> activate(X) , fst(pair(X, Y)) -> X , head(cons(N, XS)) -> N , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , sel(N, XS) -> head(afterNth(N, XS)) , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS)) , tail(cons(N, XS)) -> activate(XS) , take(N, XS) -> fst(splitAt(N, XS)) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: Arguments of following rules are not normal-forms: {splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS))} All above mentioned rules can be savely removed. We consider the following Problem: Strict Trs: { U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X)) , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , and(tt(), X) -> activate(X) , fst(pair(X, Y)) -> X , head(cons(N, XS)) -> N , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , sel(N, XS) -> head(afterNth(N, XS)) , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , tail(cons(N, XS)) -> activate(XS) , take(N, XS) -> fst(splitAt(N, XS)) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: { U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , and(tt(), X) -> activate(X) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(U11) = {}, Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(activate) = {}, Uargs(pair) = {1}, Uargs(cons) = {1}, Uargs(afterNth) = {}, Uargs(snd) = {1}, Uargs(and) = {}, Uargs(fst) = {1}, Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(n__natsFrom) = {}, Uargs(n__s) = {}, Uargs(sel) = {}, Uargs(s) = {1}, Uargs(tail) = {}, Uargs(take) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: U11(x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1] [1 0] [0 0] [0 0] [0 0] [1] tt() = [0] [0] U12(x1, x2) = [1 0] x1 + [1 0] x2 + [1] [0 0] [1 0] [1] splitAt(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] activate(x1) = [1 0] x1 + [0] [0 0] [1] pair(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] afterNth(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] snd(x1) = [1 0] x1 + [1] [0 0] [1] and(x1, x2) = [0 0] x1 + [1 0] x2 + [1] [0 0] [0 0] [1] fst(x1) = [1 0] x1 + [1] [0 0] [1] head(x1) = [1 0] x1 + [1] [0 0] [1] natsFrom(x1) = [1 0] x1 + [1] [0 0] [1] n__natsFrom(x1) = [1 0] x1 + [0] [0 0] [0] n__s(x1) = [1 0] x1 + [0] [0 0] [0] sel(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] 0() = [0] [0] nil() = [0] [0] s(x1) = [1 0] x1 + [1] [0 0] [1] tail(x1) = [1 0] x1 + [1] [0 0] [1] take(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X)) , afterNth(N, XS) -> snd(splitAt(N, XS)) , fst(pair(X, Y)) -> X , head(cons(N, XS)) -> N , sel(N, XS) -> head(afterNth(N, XS)) , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , tail(cons(N, XS)) -> activate(XS) , take(N, XS) -> fst(splitAt(N, XS)) , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X} Weak Trs: { U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , and(tt(), X) -> activate(X) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {sel(N, XS) -> head(afterNth(N, XS))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(U11) = {}, Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(activate) = {}, Uargs(pair) = {1}, Uargs(cons) = {1}, Uargs(afterNth) = {}, Uargs(snd) = {1}, Uargs(and) = {}, Uargs(fst) = {1}, Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(n__natsFrom) = {}, Uargs(n__s) = {}, Uargs(sel) = {}, Uargs(s) = {1}, Uargs(tail) = {}, Uargs(take) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: U11(x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1] [0 1] [0 0] [0 0] [0 0] [1] tt() = [0] [0] U12(x1, x2) = [1 0] x1 + [1 0] x2 + [1] [0 0] [0 0] [1] splitAt(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 1] [1] activate(x1) = [1 0] x1 + [0] [0 0] [1] pair(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [0] cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] afterNth(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] snd(x1) = [1 0] x1 + [1] [0 0] [1] and(x1, x2) = [0 0] x1 + [1 0] x2 + [1] [0 0] [0 0] [1] fst(x1) = [1 1] x1 + [1] [0 0] [1] head(x1) = [1 0] x1 + [1] [0 0] [1] natsFrom(x1) = [1 0] x1 + [1] [0 0] [1] n__natsFrom(x1) = [1 0] x1 + [0] [0 0] [0] n__s(x1) = [1 0] x1 + [0] [0 0] [0] sel(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [0 0] [0 0] [2] 0() = [0] [0] nil() = [0] [0] s(x1) = [1 0] x1 + [1] [0 0] [1] tail(x1) = [1 0] x1 + [1] [0 0] [1] take(x1, x2) = [1 0] x1 + [1 1] x2 + [0] [0 0] [0 0] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X)) , afterNth(N, XS) -> snd(splitAt(N, XS)) , fst(pair(X, Y)) -> X , head(cons(N, XS)) -> N , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , tail(cons(N, XS)) -> activate(XS) , take(N, XS) -> fst(splitAt(N, XS)) , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X} Weak Trs: { sel(N, XS) -> head(afterNth(N, XS)) , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , and(tt(), X) -> activate(X) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {take(N, XS) -> fst(splitAt(N, XS))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(U11) = {}, Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(activate) = {}, Uargs(pair) = {1}, Uargs(cons) = {1}, Uargs(afterNth) = {}, Uargs(snd) = {1}, Uargs(and) = {}, Uargs(fst) = {1}, Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(n__natsFrom) = {}, Uargs(n__s) = {}, Uargs(sel) = {}, Uargs(s) = {1}, Uargs(tail) = {}, Uargs(take) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: U11(x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1] [1 0] [0 0] [0 0] [0 0] [1] tt() = [0] [0] U12(x1, x2) = [1 0] x1 + [1 0] x2 + [1] [0 0] [1 0] [1] splitAt(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] activate(x1) = [1 0] x1 + [0] [0 0] [1] pair(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] afterNth(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] snd(x1) = [1 0] x1 + [1] [0 0] [1] and(x1, x2) = [0 0] x1 + [1 0] x2 + [1] [0 0] [0 0] [1] fst(x1) = [1 0] x1 + [1] [1 0] [1] head(x1) = [1 0] x1 + [1] [1 0] [1] natsFrom(x1) = [1 0] x1 + [1] [0 0] [1] n__natsFrom(x1) = [1 0] x1 + [0] [0 0] [0] n__s(x1) = [1 0] x1 + [0] [0 0] [0] sel(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [1 0] [1 0] [2] 0() = [0] [0] nil() = [0] [0] s(x1) = [1 0] x1 + [1] [0 0] [1] tail(x1) = [1 0] x1 + [1] [0 0] [1] take(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [1 0] [1 0] [2] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X)) , afterNth(N, XS) -> snd(splitAt(N, XS)) , fst(pair(X, Y)) -> X , head(cons(N, XS)) -> N , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , tail(cons(N, XS)) -> activate(XS) , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X} Weak Trs: { take(N, XS) -> fst(splitAt(N, XS)) , sel(N, XS) -> head(afterNth(N, XS)) , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , and(tt(), X) -> activate(X) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {afterNth(N, XS) -> snd(splitAt(N, XS))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(U11) = {}, Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(activate) = {}, Uargs(pair) = {1}, Uargs(cons) = {1}, Uargs(afterNth) = {}, Uargs(snd) = {1}, Uargs(and) = {}, Uargs(fst) = {1}, Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(n__natsFrom) = {}, Uargs(n__s) = {}, Uargs(sel) = {}, Uargs(s) = {1}, Uargs(tail) = {}, Uargs(take) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: U11(x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1] [1 0] [0 0] [0 0] [0 0] [1] tt() = [0] [0] U12(x1, x2) = [1 0] x1 + [1 0] x2 + [1] [0 0] [1 0] [1] splitAt(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] activate(x1) = [1 0] x1 + [0] [0 0] [1] pair(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] afterNth(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [0 0] [0 0] [2] snd(x1) = [1 0] x1 + [1] [0 0] [1] and(x1, x2) = [0 0] x1 + [1 0] x2 + [1] [0 0] [0 0] [1] fst(x1) = [1 0] x1 + [1] [1 0] [1] head(x1) = [1 0] x1 + [1] [1 0] [1] natsFrom(x1) = [1 0] x1 + [1] [0 0] [1] n__natsFrom(x1) = [1 0] x1 + [0] [0 0] [0] n__s(x1) = [1 0] x1 + [0] [0 0] [0] sel(x1, x2) = [1 0] x1 + [1 0] x2 + [3] [1 0] [1 0] [3] 0() = [0] [0] nil() = [0] [0] s(x1) = [1 0] x1 + [1] [0 0] [1] tail(x1) = [1 0] x1 + [1] [0 0] [1] take(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [1 0] [1 0] [2] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X)) , fst(pair(X, Y)) -> X , head(cons(N, XS)) -> N , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , tail(cons(N, XS)) -> activate(XS) , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X} Weak Trs: { afterNth(N, XS) -> snd(splitAt(N, XS)) , take(N, XS) -> fst(splitAt(N, XS)) , sel(N, XS) -> head(afterNth(N, XS)) , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , and(tt(), X) -> activate(X) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {splitAt(0(), XS) -> pair(nil(), XS)} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(U11) = {}, Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(activate) = {}, Uargs(pair) = {1}, Uargs(cons) = {1}, Uargs(afterNth) = {}, Uargs(snd) = {1}, Uargs(and) = {}, Uargs(fst) = {1}, Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(n__natsFrom) = {}, Uargs(n__s) = {}, Uargs(sel) = {}, Uargs(s) = {1}, Uargs(tail) = {}, Uargs(take) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: U11(x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1] [1 0] [0 0] [0 0] [0 0] [1] tt() = [0] [0] U12(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [1 0] [1] splitAt(x1, x2) = [1 0] x1 + [1 0] x2 + [1] [0 0] [0 0] [1] activate(x1) = [1 0] x1 + [0] [0 0] [0] pair(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] afterNth(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [0 0] [0 0] [2] snd(x1) = [1 0] x1 + [1] [0 0] [1] and(x1, x2) = [0 0] x1 + [1 0] x2 + [1] [0 0] [0 0] [1] fst(x1) = [1 0] x1 + [1] [1 0] [1] head(x1) = [1 0] x1 + [1] [1 0] [1] natsFrom(x1) = [1 0] x1 + [0] [0 0] [1] n__natsFrom(x1) = [1 0] x1 + [0] [0 0] [0] n__s(x1) = [1 0] x1 + [0] [0 0] [0] sel(x1, x2) = [1 0] x1 + [1 0] x2 + [3] [1 0] [1 0] [3] 0() = [0] [0] nil() = [0] [0] s(x1) = [1 0] x1 + [0] [0 0] [1] tail(x1) = [1 0] x1 + [1] [0 0] [1] take(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [1 0] [1 0] [2] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X)) , fst(pair(X, Y)) -> X , head(cons(N, XS)) -> N , snd(pair(X, Y)) -> Y , tail(cons(N, XS)) -> activate(XS) , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X} Weak Trs: { splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , take(N, XS) -> fst(splitAt(N, XS)) , sel(N, XS) -> head(afterNth(N, XS)) , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , and(tt(), X) -> activate(X) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {fst(pair(X, Y)) -> X} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(U11) = {}, Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(activate) = {}, Uargs(pair) = {1}, Uargs(cons) = {1}, Uargs(afterNth) = {}, Uargs(snd) = {1}, Uargs(and) = {}, Uargs(fst) = {1}, Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(n__natsFrom) = {}, Uargs(n__s) = {}, Uargs(sel) = {}, Uargs(s) = {1}, Uargs(tail) = {}, Uargs(take) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: U11(x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1] [0 1] [1 0] [0 0] [0 0] [1] tt() = [0] [0] U12(x1, x2) = [1 0] x1 + [1 0] x2 + [1] [0 0] [1 0] [0] splitAt(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] activate(x1) = [1 0] x1 + [1] [0 0] [1] pair(x1, x2) = [1 0] x1 + [0 0] x2 + [3] [0 1] [0 0] [0] cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [0] afterNth(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [2] snd(x1) = [1 0] x1 + [0] [0 0] [1] and(x1, x2) = [0 0] x1 + [1 0] x2 + [1] [0 0] [0 0] [1] fst(x1) = [1 0] x1 + [0] [0 1] [1] head(x1) = [1 0] x1 + [1] [1 0] [1] natsFrom(x1) = [1 0] x1 + [0] [0 1] [0] n__natsFrom(x1) = [1 0] x1 + [0] [0 0] [0] n__s(x1) = [1 0] x1 + [0] [0 0] [0] sel(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [1 0] [1 0] [2] 0() = [3] [0] nil() = [0] [0] s(x1) = [1 0] x1 + [0] [1 0] [0] tail(x1) = [1 0] x1 + [1] [0 0] [1] take(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [2] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X)) , head(cons(N, XS)) -> N , snd(pair(X, Y)) -> Y , tail(cons(N, XS)) -> activate(XS) , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X} Weak Trs: { fst(pair(X, Y)) -> X , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , take(N, XS) -> fst(splitAt(N, XS)) , sel(N, XS) -> head(afterNth(N, XS)) , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , and(tt(), X) -> activate(X) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(U11) = {}, Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(activate) = {}, Uargs(pair) = {1}, Uargs(cons) = {1}, Uargs(afterNth) = {}, Uargs(snd) = {1}, Uargs(and) = {}, Uargs(fst) = {1}, Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(n__natsFrom) = {}, Uargs(n__s) = {}, Uargs(sel) = {}, Uargs(s) = {1}, Uargs(tail) = {}, Uargs(take) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: U11(x1, x2, x3, x4) = [0 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1] [0 0] [0 1] [1 0] [1 0] [1] tt() = [0] [0] U12(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [1 0] [1] splitAt(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] activate(x1) = [1 0] x1 + [0] [0 0] [1] pair(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 1] [0 0] [0] cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [0] afterNth(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [0 0] [0 0] [2] snd(x1) = [1 0] x1 + [1] [0 0] [1] and(x1, x2) = [0 0] x1 + [1 0] x2 + [1] [0 0] [0 0] [1] fst(x1) = [1 0] x1 + [1] [0 1] [1] head(x1) = [1 0] x1 + [1] [1 0] [1] natsFrom(x1) = [1 0] x1 + [1] [0 1] [0] n__natsFrom(x1) = [1 0] x1 + [0] [0 0] [0] n__s(x1) = [1 0] x1 + [0] [0 0] [0] sel(x1, x2) = [1 0] x1 + [1 0] x2 + [3] [1 0] [1 0] [3] 0() = [0] [0] nil() = [0] [0] s(x1) = [1 0] x1 + [0] [1 0] [1] tail(x1) = [1 0] x1 + [1] [0 0] [1] take(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [0 0] [0 0] [2] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { head(cons(N, XS)) -> N , snd(pair(X, Y)) -> Y , tail(cons(N, XS)) -> activate(XS) , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X} Weak Trs: { U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X)) , fst(pair(X, Y)) -> X , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , take(N, XS) -> fst(splitAt(N, XS)) , sel(N, XS) -> head(afterNth(N, XS)) , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , and(tt(), X) -> activate(X) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {snd(pair(X, Y)) -> Y} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(U11) = {}, Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(activate) = {}, Uargs(pair) = {1}, Uargs(cons) = {1}, Uargs(afterNth) = {}, Uargs(snd) = {1}, Uargs(and) = {}, Uargs(fst) = {1}, Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(n__natsFrom) = {}, Uargs(n__s) = {}, Uargs(sel) = {}, Uargs(s) = {1}, Uargs(tail) = {}, Uargs(take) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: U11(x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1] [0 1] [1 0] [0 1] [0 0] [1] tt() = [0] [0] U12(x1, x2) = [1 0] x1 + [1 0] x2 + [1] [0 1] [0 0] [0] splitAt(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 1] [0] activate(x1) = [1 0] x1 + [0] [0 0] [1] pair(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 1] [0 1] [0] cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [0] afterNth(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [0 0] [0 1] [2] snd(x1) = [1 0] x1 + [1] [0 1] [1] and(x1, x2) = [0 0] x1 + [1 0] x2 + [1] [0 0] [0 0] [1] fst(x1) = [1 0] x1 + [1] [0 1] [1] head(x1) = [1 0] x1 + [1] [1 0] [1] natsFrom(x1) = [1 0] x1 + [0] [0 0] [1] n__natsFrom(x1) = [1 0] x1 + [0] [0 0] [0] n__s(x1) = [1 0] x1 + [1] [0 0] [0] sel(x1, x2) = [1 0] x1 + [1 0] x2 + [3] [1 0] [1 0] [3] 0() = [0] [0] nil() = [0] [0] s(x1) = [1 0] x1 + [1] [0 0] [1] tail(x1) = [1 0] x1 + [1] [0 0] [1] take(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [0 0] [0 1] [2] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { head(cons(N, XS)) -> N , tail(cons(N, XS)) -> activate(XS) , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X} Weak Trs: { snd(pair(X, Y)) -> Y , U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X)) , fst(pair(X, Y)) -> X , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , take(N, XS) -> fst(splitAt(N, XS)) , sel(N, XS) -> head(afterNth(N, XS)) , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , and(tt(), X) -> activate(X) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {activate(X) -> X} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(U11) = {}, Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(activate) = {}, Uargs(pair) = {1}, Uargs(cons) = {1}, Uargs(afterNth) = {}, Uargs(snd) = {1}, Uargs(and) = {}, Uargs(fst) = {1}, Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(n__natsFrom) = {}, Uargs(n__s) = {}, Uargs(sel) = {}, Uargs(s) = {1}, Uargs(tail) = {}, Uargs(take) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: U11(x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [3] [1 1] [1 1] [0 0] [1 1] [1] tt() = [2] [0] U12(x1, x2) = [1 0] x1 + [1 0] x2 + [1] [1 1] [0 0] [0] splitAt(x1, x2) = [1 0] x1 + [1 0] x2 + [1] [0 1] [0 1] [0] activate(x1) = [1 0] x1 + [1] [0 1] [0] pair(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 1] [0 1] [0] cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [0] afterNth(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [0 1] [0 1] [2] snd(x1) = [1 0] x1 + [0] [0 1] [1] and(x1, x2) = [0 0] x1 + [1 0] x2 + [1] [0 0] [0 1] [1] fst(x1) = [1 0] x1 + [1] [0 1] [1] head(x1) = [1 0] x1 + [1] [1 0] [1] natsFrom(x1) = [1 0] x1 + [0] [0 1] [1] n__natsFrom(x1) = [1 0] x1 + [0] [0 0] [1] n__s(x1) = [1 0] x1 + [0] [0 0] [0] sel(x1, x2) = [1 0] x1 + [1 0] x2 + [3] [1 0] [1 0] [3] 0() = [0] [0] nil() = [0] [0] s(x1) = [1 0] x1 + [0] [0 0] [1] tail(x1) = [1 0] x1 + [0] [0 0] [0] take(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [0 1] [0 1] [2] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { head(cons(N, XS)) -> N , tail(cons(N, XS)) -> activate(XS) , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X))} Weak Trs: { activate(X) -> X , snd(pair(X, Y)) -> Y , U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X)) , fst(pair(X, Y)) -> X , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , take(N, XS) -> fst(splitAt(N, XS)) , sel(N, XS) -> head(afterNth(N, XS)) , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , and(tt(), X) -> activate(X) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {head(cons(N, XS)) -> N} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(U11) = {}, Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(activate) = {}, Uargs(pair) = {1}, Uargs(cons) = {1}, Uargs(afterNth) = {}, Uargs(snd) = {1}, Uargs(and) = {}, Uargs(fst) = {1}, Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(n__natsFrom) = {}, Uargs(n__s) = {}, Uargs(sel) = {}, Uargs(s) = {1}, Uargs(tail) = {}, Uargs(take) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: U11(x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1] [0 1] [0 0] [0 1] [0 1] [1] tt() = [0] [0] U12(x1, x2) = [1 0] x1 + [1 0] x2 + [1] [0 1] [0 1] [1] splitAt(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 1] [0] activate(x1) = [1 0] x1 + [0] [0 1] [0] pair(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 1] [0 1] [0] cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 1] [0 0] [0] afterNth(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [0 0] [0 1] [2] snd(x1) = [1 0] x1 + [1] [0 1] [1] and(x1, x2) = [0 0] x1 + [1 0] x2 + [1] [0 0] [0 1] [1] fst(x1) = [1 0] x1 + [1] [0 1] [1] head(x1) = [1 0] x1 + [1] [0 1] [1] natsFrom(x1) = [1 0] x1 + [0] [0 1] [1] n__natsFrom(x1) = [1 0] x1 + [0] [0 0] [0] n__s(x1) = [1 0] x1 + [0] [0 0] [0] sel(x1, x2) = [1 0] x1 + [1 0] x2 + [3] [0 0] [0 1] [3] 0() = [0] [0] nil() = [0] [0] s(x1) = [1 0] x1 + [0] [0 1] [1] tail(x1) = [1 0] x1 + [1] [0 0] [1] take(x1, x2) = [1 0] x1 + [1 0] x2 + [2] [0 0] [0 1] [2] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { tail(cons(N, XS)) -> activate(XS) , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X))} Weak Trs: { head(cons(N, XS)) -> N , activate(X) -> X , snd(pair(X, Y)) -> Y , U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X)) , fst(pair(X, Y)) -> X , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , take(N, XS) -> fst(splitAt(N, XS)) , sel(N, XS) -> head(afterNth(N, XS)) , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , and(tt(), X) -> activate(X) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: { tail(cons(N, XS)) -> activate(XS) , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X))} Weak Trs: { head(cons(N, XS)) -> N , activate(X) -> X , snd(pair(X, Y)) -> Y , U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X)) , fst(pair(X, Y)) -> X , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , take(N, XS) -> fst(splitAt(N, XS)) , sel(N, XS) -> head(afterNth(N, XS)) , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , and(tt(), X) -> activate(X) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We have computed the following dependency pairs Strict DPs: { tail^#(cons(N, XS)) -> activate^#(XS) , activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) , activate^#(n__s(X)) -> s^#(activate(X))} Weak DPs: { head^#(cons(N, XS)) -> c_4() , activate^#(X) -> c_5() , snd^#(pair(X, Y)) -> c_6() , U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , fst^#(pair(X, Y)) -> c_8() , splitAt^#(0(), XS) -> c_9() , afterNth^#(N, XS) -> snd^#(splitAt(N, XS)) , take^#(N, XS) -> fst^#(splitAt(N, XS)) , sel^#(N, XS) -> head^#(afterNth(N, XS)) , U12^#(pair(YS, ZS), X) -> activate^#(X) , and^#(tt(), X) -> activate^#(X) , natsFrom^#(N) -> c_15() , natsFrom^#(X) -> c_16() , s^#(X) -> c_17()} We consider the following Problem: Strict DPs: { tail^#(cons(N, XS)) -> activate^#(XS) , activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) , activate^#(n__s(X)) -> s^#(activate(X))} Strict Trs: { tail(cons(N, XS)) -> activate(XS) , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X))} Weak DPs: { head^#(cons(N, XS)) -> c_4() , activate^#(X) -> c_5() , snd^#(pair(X, Y)) -> c_6() , U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , fst^#(pair(X, Y)) -> c_8() , splitAt^#(0(), XS) -> c_9() , afterNth^#(N, XS) -> snd^#(splitAt(N, XS)) , take^#(N, XS) -> fst^#(splitAt(N, XS)) , sel^#(N, XS) -> head^#(afterNth(N, XS)) , U12^#(pair(YS, ZS), X) -> activate^#(X) , and^#(tt(), X) -> activate^#(X) , natsFrom^#(N) -> c_15() , natsFrom^#(X) -> c_16() , s^#(X) -> c_17()} Weak Trs: { head(cons(N, XS)) -> N , activate(X) -> X , snd(pair(X, Y)) -> Y , U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X)) , fst(pair(X, Y)) -> X , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , take(N, XS) -> fst(splitAt(N, XS)) , sel(N, XS) -> head(afterNth(N, XS)) , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , and(tt(), X) -> activate(X) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We replace strict/weak-rules by the corresponding usable rules: Strict Usable Rules: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X))} Weak Usable Rules: { activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} We consider the following Problem: Strict DPs: { tail^#(cons(N, XS)) -> activate^#(XS) , activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) , activate^#(n__s(X)) -> s^#(activate(X))} Strict Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X))} Weak DPs: { head^#(cons(N, XS)) -> c_4() , activate^#(X) -> c_5() , snd^#(pair(X, Y)) -> c_6() , U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , fst^#(pair(X, Y)) -> c_8() , splitAt^#(0(), XS) -> c_9() , afterNth^#(N, XS) -> snd^#(splitAt(N, XS)) , take^#(N, XS) -> fst^#(splitAt(N, XS)) , sel^#(N, XS) -> head^#(afterNth(N, XS)) , U12^#(pair(YS, ZS), X) -> activate^#(X) , and^#(tt(), X) -> activate^#(X) , natsFrom^#(N) -> c_15() , natsFrom^#(X) -> c_16() , s^#(X) -> c_17()} Weak Trs: { activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: Dependency Pairs: { activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) , activate^#(n__s(X)) -> s^#(activate(X))} TRS Component: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X))} Interpretation of constant growth: ---------------------------------- The following argument positions are usable: Uargs(U11) = {}, Uargs(U12) = {}, Uargs(splitAt) = {1, 2}, Uargs(activate) = {}, Uargs(pair) = {}, Uargs(cons) = {}, Uargs(afterNth) = {}, Uargs(snd) = {1}, Uargs(and) = {}, Uargs(fst) = {}, Uargs(head) = {}, Uargs(natsFrom) = {1}, Uargs(n__natsFrom) = {}, Uargs(n__s) = {}, Uargs(sel) = {}, Uargs(s) = {1}, Uargs(tail) = {}, Uargs(take) = {}, Uargs(tail^#) = {}, Uargs(activate^#) = {}, Uargs(natsFrom^#) = {1}, Uargs(s^#) = {1}, Uargs(head^#) = {1}, Uargs(snd^#) = {1}, Uargs(U11^#) = {}, Uargs(U12^#) = {1, 2}, Uargs(fst^#) = {1}, Uargs(splitAt^#) = {}, Uargs(afterNth^#) = {}, Uargs(take^#) = {}, Uargs(sel^#) = {}, Uargs(and^#) = {} We have the following constructor-based EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: U11(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0] [0 0] [0 0] [0 0] [0 0] [0] tt() = [2] [1] U12(x1, x2) = [0 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [0] splitAt(x1, x2) = [2 0] x1 + [2 0] x2 + [0] [0 2] [0 1] [1] activate(x1) = [1 1] x1 + [0] [0 1] [1] pair(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 1] [0 1] [0] cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0] [0 1] [0 0] [1] afterNth(x1, x2) = [2 0] x1 + [2 0] x2 + [1] [0 2] [0 2] [2] snd(x1) = [1 0] x1 + [1] [0 1] [1] and(x1, x2) = [0 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [0] fst(x1) = [0 0] x1 + [0] [0 0] [0] head(x1) = [0 0] x1 + [0] [0 0] [0] natsFrom(x1) = [1 0] x1 + [0] [0 1] [2] n__natsFrom(x1) = [1 0] x1 + [0] [0 1] [2] n__s(x1) = [1 0] x1 + [0] [0 1] [2] sel(x1, x2) = [0 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [0] 0() = [0] [0] nil() = [0] [0] s(x1) = [1 0] x1 + [1] [0 1] [2] tail(x1) = [0 0] x1 + [0] [0 0] [0] take(x1, x2) = [0 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [0] tail^#(x1) = [2 2] x1 + [0] [0 0] [0] activate^#(x1) = [1 1] x1 + [0] [0 0] [0] natsFrom^#(x1) = [1 0] x1 + [0] [0 0] [0] s^#(x1) = [1 0] x1 + [0] [0 0] [0] head^#(x1) = [1 0] x1 + [1] [0 0] [1] c_4() = [0] [0] c_5() = [0] [0] snd^#(x1) = [1 0] x1 + [1] [0 0] [0] c_6() = [0] [0] U11^#(x1, x2, x3, x4) = [0 0] x1 + [2 2] x2 + [2 2] x3 + [2 2] x4 + [1] [0 0] [0 0] [0 0] [0 0] [1] U12^#(x1, x2) = [1 0] x1 + [1 1] x2 + [0] [0 0] [0 0] [1] fst^#(x1) = [1 1] x1 + [0] [0 0] [1] c_8() = [0] [0] splitAt^#(x1, x2) = [0 0] x1 + [0 0] x2 + [1] [0 0] [0 0] [1] c_9() = [0] [0] afterNth^#(x1, x2) = [2 0] x1 + [2 0] x2 + [2] [0 0] [0 0] [0] take^#(x1, x2) = [2 2] x1 + [2 2] x2 + [2] [0 0] [0 0] [2] sel^#(x1, x2) = [2 0] x1 + [2 0] x2 + [2] [0 0] [0 0] [2] and^#(x1, x2) = [0 0] x1 + [2 2] x2 + [1] [3 2] [0 0] [1] c_15() = [0] [0] c_16() = [0] [0] c_17() = [0] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict DPs: {tail^#(cons(N, XS)) -> activate^#(XS)} Weak DPs: { activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) , activate^#(n__s(X)) -> s^#(activate(X)) , head^#(cons(N, XS)) -> c_4() , activate^#(X) -> c_5() , snd^#(pair(X, Y)) -> c_6() , U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , fst^#(pair(X, Y)) -> c_8() , splitAt^#(0(), XS) -> c_9() , afterNth^#(N, XS) -> snd^#(splitAt(N, XS)) , take^#(N, XS) -> fst^#(splitAt(N, XS)) , sel^#(N, XS) -> head^#(afterNth(N, XS)) , U12^#(pair(YS, ZS), X) -> activate^#(X) , and^#(tt(), X) -> activate^#(X) , natsFrom^#(N) -> c_15() , natsFrom^#(X) -> c_16() , s^#(X) -> c_17()} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We use following congruence DG for path analysis ->11:{1} [ YES(O(1),O(1)) ] | |->13:{2} [ subsumed ] | | | |->14:{15} [ YES(O(1),O(1)) ] | | | `->15:{16} [ YES(O(1),O(1)) ] | |->16:{3} [ subsumed ] | | | `->17:{17} [ YES(O(1),O(1)) ] | `->12:{5} [ YES(O(1),O(1)) ] ->7:{7} [ subsumed ] | `->8:{13} [ subsumed ] | |->13:{2} [ subsumed ] | | | |->14:{15} [ YES(O(1),O(1)) ] | | | `->15:{16} [ YES(O(1),O(1)) ] | |->16:{3} [ subsumed ] | | | `->17:{17} [ YES(O(1),O(1)) ] | `->12:{5} [ YES(O(1),O(1)) ] ->5:{9} [ YES(O(1),O(1)) ] ->4:{10} [ subsumed ] | `->9:{6} [ YES(O(1),O(1)) ] ->3:{11} [ subsumed ] | `->6:{8} [ YES(O(1),O(1)) ] ->2:{12} [ subsumed ] | `->10:{4} [ YES(O(1),O(1)) ] ->1:{14} [ subsumed ] | |->13:{2} [ subsumed ] | | | |->14:{15} [ YES(O(1),O(1)) ] | | | `->15:{16} [ YES(O(1),O(1)) ] | |->16:{3} [ subsumed ] | | | `->17:{17} [ YES(O(1),O(1)) ] | `->12:{5} [ YES(O(1),O(1)) ] Here dependency-pairs are as follows: Strict DPs: {1: tail^#(cons(N, XS)) -> activate^#(XS)} WeakDPs DPs: { 2: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) , 3: activate^#(n__s(X)) -> s^#(activate(X)) , 4: head^#(cons(N, XS)) -> c_4() , 5: activate^#(X) -> c_5() , 6: snd^#(pair(X, Y)) -> c_6() , 7: U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , 8: fst^#(pair(X, Y)) -> c_8() , 9: splitAt^#(0(), XS) -> c_9() , 10: afterNth^#(N, XS) -> snd^#(splitAt(N, XS)) , 11: take^#(N, XS) -> fst^#(splitAt(N, XS)) , 12: sel^#(N, XS) -> head^#(afterNth(N, XS)) , 13: U12^#(pair(YS, ZS), X) -> activate^#(X) , 14: and^#(tt(), X) -> activate^#(X) , 15: natsFrom^#(N) -> c_15() , 16: natsFrom^#(X) -> c_16() , 17: s^#(X) -> c_17()} * Path 11:{1}: YES(O(1),O(1)) --------------------------- We consider the following Problem: Strict DPs: {tail^#(cons(N, XS)) -> activate^#(XS)} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: tail^#(cons(N, XS)) -> activate^#(XS) together with the congruence-graph ->1:{1} Noncyclic, trivial, SCC Here dependency-pairs are as follows: Strict DPs: {1: tail^#(cons(N, XS)) -> activate^#(XS)} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: {1: tail^#(cons(N, XS)) -> activate^#(XS)} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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 11:{1}->13:{2}: subsumed ----------------------------- This path is subsumed by the proof of paths 11:{1}->13:{2}->15:{16}, 11:{1}->13:{2}->14:{15}. * Path 11:{1}->13:{2}->14:{15}: YES(O(1),O(1)) -------------------------------------------- We consider the following Problem: Weak DPs: { tail^#(cons(N, XS)) -> activate^#(XS) , activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: tail^#(cons(N, XS)) -> activate^#(XS) -->_1 activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) :2 2: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) together with the congruence-graph ->1:{1} Weak SCC | `->2:{2} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: { 1: tail^#(cons(N, XS)) -> activate^#(XS) , 2: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: { 1: tail^#(cons(N, XS)) -> activate^#(XS) , 2: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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 11:{1}->13:{2}->15:{16}: YES(O(1),O(1)) -------------------------------------------- We consider the following Problem: Weak DPs: { tail^#(cons(N, XS)) -> activate^#(XS) , activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: tail^#(cons(N, XS)) -> activate^#(XS) -->_1 activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) :2 2: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) together with the congruence-graph ->1:{1} Weak SCC | `->2:{2} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: { 1: tail^#(cons(N, XS)) -> activate^#(XS) , 2: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: { 1: tail^#(cons(N, XS)) -> activate^#(XS) , 2: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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 11:{1}->16:{3}: subsumed ----------------------------- This path is subsumed by the proof of paths 11:{1}->16:{3}->17:{17}. * Path 11:{1}->16:{3}->17:{17}: YES(O(1),O(1)) -------------------------------------------- We consider the following Problem: Weak DPs: { tail^#(cons(N, XS)) -> activate^#(XS) , activate^#(n__s(X)) -> s^#(activate(X))} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: tail^#(cons(N, XS)) -> activate^#(XS) -->_1 activate^#(n__s(X)) -> s^#(activate(X)) :2 2: activate^#(n__s(X)) -> s^#(activate(X)) together with the congruence-graph ->1:{1} Weak SCC | `->2:{2} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: { 1: tail^#(cons(N, XS)) -> activate^#(XS) , 2: activate^#(n__s(X)) -> s^#(activate(X))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: { 1: tail^#(cons(N, XS)) -> activate^#(XS) , 2: activate^#(n__s(X)) -> s^#(activate(X))} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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 11:{1}->12:{5}: YES(O(1),O(1)) ----------------------------------- We consider the following Problem: Weak DPs: {tail^#(cons(N, XS)) -> activate^#(XS)} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: tail^#(cons(N, XS)) -> activate^#(XS) together with the congruence-graph ->1:{1} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: {1: tail^#(cons(N, XS)) -> activate^#(XS)} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: {1: tail^#(cons(N, XS)) -> activate^#(XS)} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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 7:{7}: subsumed -------------------- This path is subsumed by the proof of paths 7:{7}->8:{13}. * Path 7:{7}->8:{13}: subsumed ---------------------------- This path is subsumed by the proof of paths 7:{7}->8:{13}->16:{3}, 7:{7}->8:{13}->13:{2}, 7:{7}->8:{13}->12:{5}. * Path 7:{7}->8:{13}->13:{2}: subsumed ------------------------------------ This path is subsumed by the proof of paths 7:{7}->8:{13}->13:{2}->15:{16}, 7:{7}->8:{13}->13:{2}->14:{15}. * Path 7:{7}->8:{13}->13:{2}->14:{15}: YES(O(1),O(1)) --------------------------------------------------- We consider the following Problem: Weak DPs: { U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , U12^#(pair(YS, ZS), X) -> activate^#(X) , activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) -->_1 U12^#(pair(YS, ZS), X) -> activate^#(X) :2 2: U12^#(pair(YS, ZS), X) -> activate^#(X) -->_1 activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) :3 3: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) together with the congruence-graph ->1:{1} Weak SCC | `->2:{2} Weak SCC | `->3:{3} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: { 1: U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , 2: U12^#(pair(YS, ZS), X) -> activate^#(X) , 3: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: { 1: U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , 2: U12^#(pair(YS, ZS), X) -> activate^#(X) , 3: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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 7:{7}->8:{13}->13:{2}->15:{16}: YES(O(1),O(1)) --------------------------------------------------- We consider the following Problem: Weak DPs: { U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , U12^#(pair(YS, ZS), X) -> activate^#(X) , activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) -->_1 U12^#(pair(YS, ZS), X) -> activate^#(X) :2 2: U12^#(pair(YS, ZS), X) -> activate^#(X) -->_1 activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) :3 3: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) together with the congruence-graph ->1:{1} Weak SCC | `->2:{2} Weak SCC | `->3:{3} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: { 1: U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , 2: U12^#(pair(YS, ZS), X) -> activate^#(X) , 3: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: { 1: U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , 2: U12^#(pair(YS, ZS), X) -> activate^#(X) , 3: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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 7:{7}->8:{13}->16:{3}: subsumed ------------------------------------ This path is subsumed by the proof of paths 7:{7}->8:{13}->16:{3}->17:{17}. * Path 7:{7}->8:{13}->16:{3}->17:{17}: YES(O(1),O(1)) --------------------------------------------------- We consider the following Problem: Weak DPs: { U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , U12^#(pair(YS, ZS), X) -> activate^#(X) , activate^#(n__s(X)) -> s^#(activate(X))} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) -->_1 U12^#(pair(YS, ZS), X) -> activate^#(X) :2 2: U12^#(pair(YS, ZS), X) -> activate^#(X) -->_1 activate^#(n__s(X)) -> s^#(activate(X)) :3 3: activate^#(n__s(X)) -> s^#(activate(X)) together with the congruence-graph ->1:{1} Weak SCC | `->2:{2} Weak SCC | `->3:{3} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: { 1: U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , 2: U12^#(pair(YS, ZS), X) -> activate^#(X) , 3: activate^#(n__s(X)) -> s^#(activate(X))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: { 1: U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , 2: U12^#(pair(YS, ZS), X) -> activate^#(X) , 3: activate^#(n__s(X)) -> s^#(activate(X))} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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 7:{7}->8:{13}->12:{5}: YES(O(1),O(1)) ------------------------------------------ We consider the following Problem: Weak DPs: { U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , U12^#(pair(YS, ZS), X) -> activate^#(X)} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) -->_1 U12^#(pair(YS, ZS), X) -> activate^#(X) :2 2: U12^#(pair(YS, ZS), X) -> activate^#(X) together with the congruence-graph ->1:{1} Weak SCC | `->2:{2} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: { 1: U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , 2: U12^#(pair(YS, ZS), X) -> activate^#(X)} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: { 1: U11^#(tt(), N, X, XS) -> U12^#(splitAt(activate(N), activate(XS)), activate(X)) , 2: U12^#(pair(YS, ZS), X) -> activate^#(X)} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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 5:{9}: YES(O(1),O(1)) -------------------------- We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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:{10}: subsumed --------------------- This path is subsumed by the proof of paths 4:{10}->9:{6}. * Path 4:{10}->9:{6}: YES(O(1),O(1)) ---------------------------------- We consider the following Problem: Weak DPs: {afterNth^#(N, XS) -> snd^#(splitAt(N, XS))} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: afterNth^#(N, XS) -> snd^#(splitAt(N, XS)) together with the congruence-graph ->1:{1} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: {1: afterNth^#(N, XS) -> snd^#(splitAt(N, XS))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: {1: afterNth^#(N, XS) -> snd^#(splitAt(N, XS))} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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 3:{11}: subsumed --------------------- This path is subsumed by the proof of paths 3:{11}->6:{8}. * Path 3:{11}->6:{8}: YES(O(1),O(1)) ---------------------------------- We consider the following Problem: Weak DPs: {take^#(N, XS) -> fst^#(splitAt(N, XS))} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: take^#(N, XS) -> fst^#(splitAt(N, XS)) together with the congruence-graph ->1:{1} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: {1: take^#(N, XS) -> fst^#(splitAt(N, XS))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: {1: take^#(N, XS) -> fst^#(splitAt(N, XS))} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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:{12}: subsumed --------------------- This path is subsumed by the proof of paths 2:{12}->10:{4}. * Path 2:{12}->10:{4}: YES(O(1),O(1)) ----------------------------------- We consider the following Problem: Weak DPs: {sel^#(N, XS) -> head^#(afterNth(N, XS))} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: sel^#(N, XS) -> head^#(afterNth(N, XS)) together with the congruence-graph ->1:{1} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: {1: sel^#(N, XS) -> head^#(afterNth(N, XS))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: {1: sel^#(N, XS) -> head^#(afterNth(N, XS))} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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:{14}: subsumed --------------------- This path is subsumed by the proof of paths 1:{14}->16:{3}, 1:{14}->13:{2}, 1:{14}->12:{5}. * Path 1:{14}->13:{2}: subsumed ----------------------------- This path is subsumed by the proof of paths 1:{14}->13:{2}->15:{16}, 1:{14}->13:{2}->14:{15}. * Path 1:{14}->13:{2}->14:{15}: YES(O(1),O(1)) -------------------------------------------- We consider the following Problem: Weak DPs: { and^#(tt(), X) -> activate^#(X) , activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: and^#(tt(), X) -> activate^#(X) -->_1 activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) :2 2: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) together with the congruence-graph ->1:{1} Weak SCC | `->2:{2} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: { 1: and^#(tt(), X) -> activate^#(X) , 2: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: { 1: and^#(tt(), X) -> activate^#(X) , 2: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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:{14}->13:{2}->15:{16}: YES(O(1),O(1)) -------------------------------------------- We consider the following Problem: Weak DPs: { and^#(tt(), X) -> activate^#(X) , activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: and^#(tt(), X) -> activate^#(X) -->_1 activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) :2 2: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X)) together with the congruence-graph ->1:{1} Weak SCC | `->2:{2} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: { 1: and^#(tt(), X) -> activate^#(X) , 2: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: { 1: and^#(tt(), X) -> activate^#(X) , 2: activate^#(n__natsFrom(X)) -> natsFrom^#(activate(X))} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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:{14}->16:{3}: subsumed ----------------------------- This path is subsumed by the proof of paths 1:{14}->16:{3}->17:{17}. * Path 1:{14}->16:{3}->17:{17}: YES(O(1),O(1)) -------------------------------------------- We consider the following Problem: Weak DPs: { and^#(tt(), X) -> activate^#(X) , activate^#(n__s(X)) -> s^#(activate(X))} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: and^#(tt(), X) -> activate^#(X) -->_1 activate^#(n__s(X)) -> s^#(activate(X)) :2 2: activate^#(n__s(X)) -> s^#(activate(X)) together with the congruence-graph ->1:{1} Weak SCC | `->2:{2} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: { 1: and^#(tt(), X) -> activate^#(X) , 2: activate^#(n__s(X)) -> s^#(activate(X))} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: { 1: and^#(tt(), X) -> activate^#(X) , 2: activate^#(n__s(X)) -> s^#(activate(X))} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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:{14}->12:{5}: YES(O(1),O(1)) ----------------------------------- We consider the following Problem: Weak DPs: {and^#(tt(), X) -> activate^#(X)} Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the the dependency-graph 1: and^#(tt(), X) -> activate^#(X) together with the congruence-graph ->1:{1} Weak SCC Here dependency-pairs are as follows: WeakDPs DPs: {1: and^#(tt(), X) -> activate^#(X)} The following rules are either leafs or part of trailing weak paths, and thus they can be removed: {1: and^#(tt(), X) -> activate^#(X)} We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(O(1),O(1)) Proof: We consider the following Problem: Weak Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(X) -> X , snd(pair(X, Y)) -> Y , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> snd(splitAt(N, XS)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X)} 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))