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