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