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