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