YES TRS: { a__fst(X1, X2) -> fst(X1, X2), a__fst(0(), Z) -> nil(), a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)), mark(nil()) -> nil(), mark(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)), mark(s(X)) -> s(X), mark(from(X)) -> a__from(mark(X)), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(len(X)) -> a__len(mark(X)), a__from(X) -> cons(mark(X), from(s(X))), a__from(X) -> from(X), a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark(X), a__add(s(X), Y) -> s(add(X, Y)), a__len(X) -> len(X), a__len(nil()) -> 0(), a__len(cons(X, Z)) -> s(len(Z))} DP: Strict: {a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)), mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X), mark#(from(X)) -> a__from#(mark(X)), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), mark#(len(X)) -> mark#(X), mark#(len(X)) -> a__len#(mark(X)), a__from#(X) -> mark#(X), a__add#(0(), X) -> mark#(X)} Weak: { a__fst(X1, X2) -> fst(X1, X2), a__fst(0(), Z) -> nil(), a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)), mark(nil()) -> nil(), mark(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)), mark(s(X)) -> s(X), mark(from(X)) -> a__from(mark(X)), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(len(X)) -> a__len(mark(X)), a__from(X) -> cons(mark(X), from(s(X))), a__from(X) -> from(X), a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark(X), a__add(s(X), Y) -> s(add(X, Y)), a__len(X) -> len(X), a__len(nil()) -> 0(), a__len(cons(X, Z)) -> s(len(Z))} EDG: {(mark#(add(X1, X2)) -> mark#(X2), mark#(len(X)) -> a__len#(mark(X))) (mark#(add(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X2), mark#(from(X)) -> a__from#(mark(X))) (mark#(add(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(len(X)) -> mark#(X), mark#(len(X)) -> a__len#(mark(X))) (mark#(len(X)) -> mark#(X), mark#(len(X)) -> mark#(X)) (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (mark#(len(X)) -> mark#(X), mark#(from(X)) -> a__from#(mark(X))) (mark#(len(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(len(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (a__add#(0(), X) -> mark#(X), mark#(len(X)) -> a__len#(mark(X))) (a__add#(0(), X) -> mark#(X), mark#(len(X)) -> mark#(X)) (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (a__add#(0(), X) -> mark#(X), mark#(from(X)) -> a__from#(mark(X))) (a__add#(0(), X) -> mark#(X), mark#(from(X)) -> mark#(X)) (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2)) (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1)) (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (a__add#(0(), X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(0(), X) -> mark#(X)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> a__len#(mark(X))) (mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(from(X)) -> a__from#(mark(X))) (mark#(fst(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(len(X)) -> a__len#(mark(X))) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(len(X)) -> mark#(X)) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X2)) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X1)) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(from(X)) -> a__from#(mark(X))) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(from(X)) -> mark#(X)) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(fst(X1, X2)) -> mark#(X2)) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(fst(X1, X2)) -> mark#(X1)) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X1), mark#(from(X)) -> a__from#(mark(X))) (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X1), mark#(len(X)) -> a__len#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> a__from#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(len(X)) -> a__len#(mark(X))) (mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)), a__fst#(s(X), cons(Y, Z)) -> mark#(Y)) (mark#(from(X)) -> a__from#(mark(X)), a__from#(X) -> mark#(X)) (a__from#(X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (a__from#(X) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (a__from#(X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1)) (a__from#(X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2)) (a__from#(X) -> mark#(X), mark#(from(X)) -> mark#(X)) (a__from#(X) -> mark#(X), mark#(from(X)) -> a__from#(mark(X))) (a__from#(X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (a__from#(X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (a__from#(X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (a__from#(X) -> mark#(X), mark#(len(X)) -> mark#(X)) (a__from#(X) -> mark#(X), mark#(len(X)) -> a__len#(mark(X))) (mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(from(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(from(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(from(X)) -> a__from#(mark(X))) (mark#(from(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (mark#(from(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(from(X)) -> mark#(X), mark#(len(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(len(X)) -> a__len#(mark(X))) (mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(from(X)) -> a__from#(mark(X))) (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> a__len#(mark(X)))} SCCS: Scc: {a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)), mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X), mark#(from(X)) -> a__from#(mark(X)), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), mark#(len(X)) -> mark#(X), a__from#(X) -> mark#(X), a__add#(0(), X) -> mark#(X)} SCC: Strict: {a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)), mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X), mark#(from(X)) -> a__from#(mark(X)), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), mark#(len(X)) -> mark#(X), a__from#(X) -> mark#(X), a__add#(0(), X) -> mark#(X)} Weak: { a__fst(X1, X2) -> fst(X1, X2), a__fst(0(), Z) -> nil(), a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)), mark(nil()) -> nil(), mark(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)), mark(s(X)) -> s(X), mark(from(X)) -> a__from(mark(X)), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(len(X)) -> a__len(mark(X)), a__from(X) -> cons(mark(X), from(s(X))), a__from(X) -> from(X), a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark(X), a__add(s(X), Y) -> s(add(X, Y)), a__len(X) -> len(X), a__len(nil()) -> 0(), a__len(cons(X, Z)) -> s(len(Z))} POLY: Argument Filtering: pi(len) = 0, pi(a__len) = 0, pi(add) = [0,1], pi(a__add#) = 1, pi(a__add) = [0,1], pi(a__from#) = 0, pi(a__from) = [0], pi(from) = [0], pi(s) = [], pi(fst) = [0,1], pi(mark#) = 0, pi(mark) = 0, pi(cons) = 0, pi(0) = [], pi(a__fst#) = 1, pi(a__fst) = [0,1], pi(nil) = [] Usable Rules: {} Interpretation: [add](x0, x1) = x0 + x1, [fst](x0, x1) = x0 + x1, [from](x0) = x0 + 1 Strict: {a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)), mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), mark#(len(X)) -> mark#(X), a__from#(X) -> mark#(X), a__add#(0(), X) -> mark#(X)} Weak: { a__fst(X1, X2) -> fst(X1, X2), a__fst(0(), Z) -> nil(), a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)), mark(nil()) -> nil(), mark(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)), mark(s(X)) -> s(X), mark(from(X)) -> a__from(mark(X)), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(len(X)) -> a__len(mark(X)), a__from(X) -> cons(mark(X), from(s(X))), a__from(X) -> from(X), a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark(X), a__add(s(X), Y) -> s(add(X, Y)), a__len(X) -> len(X), a__len(nil()) -> 0(), a__len(cons(X, Z)) -> s(len(Z))} EDG: {(mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(0(), X) -> mark#(X)) (mark#(len(X)) -> mark#(X), mark#(len(X)) -> mark#(X)) (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(len(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (a__add#(0(), X) -> mark#(X), mark#(len(X)) -> mark#(X)) (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2)) (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1)) (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (a__add#(0(), X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X)) (a__from#(X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (a__from#(X) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (a__from#(X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1)) (a__from#(X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2)) (a__from#(X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (a__from#(X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (a__from#(X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (a__from#(X) -> mark#(X), mark#(len(X)) -> mark#(X)) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1)) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(fst(X1, X2)) -> mark#(X1)) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(fst(X1, X2)) -> mark#(X2)) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X1)) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X2)) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(len(X)) -> mark#(X)) (mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)), a__fst#(s(X), cons(Y, Z)) -> mark#(Y))} SCCS: Scc: {a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)), mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), mark#(len(X)) -> mark#(X), a__add#(0(), X) -> mark#(X)} SCC: Strict: {a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)), mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), mark#(len(X)) -> mark#(X), a__add#(0(), X) -> mark#(X)} Weak: { a__fst(X1, X2) -> fst(X1, X2), a__fst(0(), Z) -> nil(), a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)), mark(nil()) -> nil(), mark(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)), mark(s(X)) -> s(X), mark(from(X)) -> a__from(mark(X)), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(len(X)) -> a__len(mark(X)), a__from(X) -> cons(mark(X), from(s(X))), a__from(X) -> from(X), a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark(X), a__add(s(X), Y) -> s(add(X, Y)), a__len(X) -> len(X), a__len(nil()) -> 0(), a__len(cons(X, Z)) -> s(len(Z))} POLY: Argument Filtering: pi(len) = 0, pi(a__len) = 0, pi(add) = [0,1], pi(a__add#) = 1, pi(a__add) = [0,1], pi(a__from) = [0], pi(from) = [0], pi(s) = [], pi(fst) = [0,1], pi(mark#) = 0, pi(mark) = 0, pi(cons) = [0], pi(0) = [], pi(a__fst#) = 1, pi(a__fst) = [0,1], pi(nil) = [] Usable Rules: {} Interpretation: [add](x0, x1) = x0 + x1, [fst](x0, x1) = x0 + x1, [cons](x0) = x0 + 1 Strict: {mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)), mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), mark#(len(X)) -> mark#(X), a__add#(0(), X) -> mark#(X)} Weak: { a__fst(X1, X2) -> fst(X1, X2), a__fst(0(), Z) -> nil(), a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)), mark(nil()) -> nil(), mark(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)), mark(s(X)) -> s(X), mark(from(X)) -> a__from(mark(X)), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(len(X)) -> a__len(mark(X)), a__from(X) -> cons(mark(X), from(s(X))), a__from(X) -> from(X), a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark(X), a__add(s(X), Y) -> s(add(X, Y)), a__len(X) -> len(X), a__len(nil()) -> 0(), a__len(cons(X, Z)) -> s(len(Z))} EDG: {(mark#(add(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(0(), X) -> mark#(X)) (a__add#(0(), X) -> mark#(X), mark#(len(X)) -> mark#(X)) (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2)) (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1)) (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(len(X)) -> mark#(X), mark#(len(X)) -> mark#(X)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2))) (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2))) (mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X))} SCCS: Scc: {mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), mark#(len(X)) -> mark#(X), a__add#(0(), X) -> mark#(X)} SCC: Strict: {mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), mark#(len(X)) -> mark#(X), a__add#(0(), X) -> mark#(X)} Weak: { a__fst(X1, X2) -> fst(X1, X2), a__fst(0(), Z) -> nil(), a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)), mark(nil()) -> nil(), mark(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)), mark(s(X)) -> s(X), mark(from(X)) -> a__from(mark(X)), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(len(X)) -> a__len(mark(X)), a__from(X) -> cons(mark(X), from(s(X))), a__from(X) -> from(X), a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark(X), a__add(s(X), Y) -> s(add(X, Y)), a__len(X) -> len(X), a__len(nil()) -> 0(), a__len(cons(X, Z)) -> s(len(Z))} POLY: Argument Filtering: pi(len) = 0, pi(a__len) = 0, pi(add) = [0,1], pi(a__add#) = 1, pi(a__add) = [0,1], pi(a__from) = [], pi(from) = [], pi(s) = [], pi(fst) = [0,1], pi(mark#) = 0, pi(mark) = 0, pi(cons) = [], pi(0) = [], pi(a__fst) = [0,1], pi(nil) = [] Usable Rules: {} Interpretation: [add](x0, x1) = x0 + x1 + 1, [fst](x0, x1) = x0 + x1 Strict: {mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X), a__add#(0(), X) -> mark#(X)} Weak: { a__fst(X1, X2) -> fst(X1, X2), a__fst(0(), Z) -> nil(), a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)), mark(nil()) -> nil(), mark(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)), mark(s(X)) -> s(X), mark(from(X)) -> a__from(mark(X)), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(len(X)) -> a__len(mark(X)), a__from(X) -> cons(mark(X), from(s(X))), a__from(X) -> from(X), a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark(X), a__add(s(X), Y) -> s(add(X, Y)), a__len(X) -> len(X), a__len(nil()) -> 0(), a__len(cons(X, Z)) -> s(len(Z))} EDG: {(mark#(len(X)) -> mark#(X), mark#(len(X)) -> mark#(X)) (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1)) (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1)) (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2)) (a__add#(0(), X) -> mark#(X), mark#(len(X)) -> mark#(X)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2)) (mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X))} SCCS: Scc: {mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X)} SCC: Strict: {mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X)} Weak: { a__fst(X1, X2) -> fst(X1, X2), a__fst(0(), Z) -> nil(), a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)), mark(nil()) -> nil(), mark(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)), mark(s(X)) -> s(X), mark(from(X)) -> a__from(mark(X)), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(len(X)) -> a__len(mark(X)), a__from(X) -> cons(mark(X), from(s(X))), a__from(X) -> from(X), a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark(X), a__add(s(X), Y) -> s(add(X, Y)), a__len(X) -> len(X), a__len(nil()) -> 0(), a__len(cons(X, Z)) -> s(len(Z))} SPSC: Simple Projection: pi(mark#) = 0 Strict: {mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X)} EDG: {(mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X)) (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1)) (mark#(len(X)) -> mark#(X), mark#(len(X)) -> mark#(X))} SCCS: Scc: {mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X)} SCC: Strict: {mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X)} Weak: { a__fst(X1, X2) -> fst(X1, X2), a__fst(0(), Z) -> nil(), a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)), mark(nil()) -> nil(), mark(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)), mark(s(X)) -> s(X), mark(from(X)) -> a__from(mark(X)), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(len(X)) -> a__len(mark(X)), a__from(X) -> cons(mark(X), from(s(X))), a__from(X) -> from(X), a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark(X), a__add(s(X), Y) -> s(add(X, Y)), a__len(X) -> len(X), a__len(nil()) -> 0(), a__len(cons(X, Z)) -> s(len(Z))} SPSC: Simple Projection: pi(mark#) = 0 Strict: {mark#(len(X)) -> mark#(X)} EDG: {(mark#(len(X)) -> mark#(X), mark#(len(X)) -> mark#(X))} SCCS: Scc: {mark#(len(X)) -> mark#(X)} SCC: Strict: {mark#(len(X)) -> mark#(X)} Weak: { a__fst(X1, X2) -> fst(X1, X2), a__fst(0(), Z) -> nil(), a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)), mark(nil()) -> nil(), mark(0()) -> 0(), mark(cons(X1, X2)) -> cons(mark(X1), X2), mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)), mark(s(X)) -> s(X), mark(from(X)) -> a__from(mark(X)), mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)), mark(len(X)) -> a__len(mark(X)), a__from(X) -> cons(mark(X), from(s(X))), a__from(X) -> from(X), a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark(X), a__add(s(X), Y) -> s(add(X, Y)), a__len(X) -> len(X), a__len(nil()) -> 0(), a__len(cons(X, Z)) -> s(len(Z))} SPSC: Simple Projection: pi(mark#) = 0 Strict: {} Qed