MAYBE TRS: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} DP: Strict: { __#(X1, mark(X2)) -> __#(X1, X2), __#(mark(X1), X2) -> __#(X1, X2), __#(ok(X1), ok(X2)) -> __#(X1, X2), active#(__(X1, X2)) -> __#(X1, active(X2)), active#(__(X1, X2)) -> __#(active(X1), X2), active#(__(X1, X2)) -> active#(X1), active#(__(X1, X2)) -> active#(X2), active#(__(__(X, Y), Z)) -> __#(X, __(Y, Z)), active#(__(__(X, Y), Z)) -> __#(Y, Z), active#(and(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> and#(active(X1), X2), active#(isNeList(V)) -> isQid#(V), active#(isNeList(__(V1, V2))) -> and#(isNeList(V1), isList(V2)), active#(isNeList(__(V1, V2))) -> and#(isList(V1), isNeList(V2)), active#(isNeList(__(V1, V2))) -> isNeList#(V1), active#(isNeList(__(V1, V2))) -> isNeList#(V2), active#(isNeList(__(V1, V2))) -> isList#(V1), active#(isNeList(__(V1, V2))) -> isList#(V2), active#(isList(V)) -> isNeList#(V), active#(isList(__(V1, V2))) -> and#(isList(V1), isList(V2)), active#(isList(__(V1, V2))) -> isList#(V1), active#(isList(__(V1, V2))) -> isList#(V2), active#(isNePal(V)) -> isQid#(V), active#(isNePal(__(I, __(P, I)))) -> and#(isQid(I), isPal(P)), active#(isNePal(__(I, __(P, I)))) -> isQid#(I), active#(isNePal(__(I, __(P, I)))) -> isPal#(P), active#(isPal(V)) -> isNePal#(V), and#(mark(X1), X2) -> and#(X1, X2), and#(ok(X1), ok(X2)) -> and#(X1, X2), isNeList#(ok(X)) -> isNeList#(X), isList#(ok(X)) -> isList#(X), isQid#(ok(X)) -> isQid#(X), isNePal#(ok(X)) -> isNePal#(X), isPal#(ok(X)) -> isPal#(X), proper#(__(X1, X2)) -> __#(proper(X1), proper(X2)), proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)), proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> isNeList#(proper(X)), proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> isList#(proper(X)), proper#(isList(X)) -> proper#(X), proper#(isQid(X)) -> isQid#(proper(X)), proper#(isQid(X)) -> proper#(X), proper#(isNePal(X)) -> isNePal#(proper(X)), proper#(isNePal(X)) -> proper#(X), proper#(isPal(X)) -> isPal#(proper(X)), proper#(isPal(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: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} EDG: { (active#(isNeList(__(V1, V2))) -> isList#(V1), isList#(ok(X)) -> isList#(X)) (active#(__(X1, X2)) -> active#(X1), active#(isPal(V)) -> isNePal#(V)) (active#(__(X1, X2)) -> active#(X1), active#(isNePal(__(I, __(P, I)))) -> isPal#(P)) (active#(__(X1, X2)) -> active#(X1), active#(isNePal(__(I, __(P, I)))) -> isQid#(I)) (active#(__(X1, X2)) -> active#(X1), active#(isNePal(__(I, __(P, I)))) -> and#(isQid(I), isPal(P))) (active#(__(X1, X2)) -> active#(X1), active#(isNePal(V)) -> isQid#(V)) (active#(__(X1, X2)) -> active#(X1), active#(isList(__(V1, V2))) -> isList#(V2)) (active#(__(X1, X2)) -> active#(X1), active#(isList(__(V1, V2))) -> isList#(V1)) (active#(__(X1, X2)) -> active#(X1), active#(isList(__(V1, V2))) -> and#(isList(V1), isList(V2))) (active#(__(X1, X2)) -> active#(X1), active#(isList(V)) -> isNeList#(V)) (active#(__(X1, X2)) -> active#(X1), active#(isNeList(__(V1, V2))) -> isList#(V2)) (active#(__(X1, X2)) -> active#(X1), active#(isNeList(__(V1, V2))) -> isList#(V1)) (active#(__(X1, X2)) -> active#(X1), active#(isNeList(__(V1, V2))) -> isNeList#(V2)) (active#(__(X1, X2)) -> active#(X1), active#(isNeList(__(V1, V2))) -> isNeList#(V1)) (active#(__(X1, X2)) -> active#(X1), active#(isNeList(__(V1, V2))) -> and#(isList(V1), isNeList(V2))) (active#(__(X1, X2)) -> active#(X1), active#(isNeList(__(V1, V2))) -> and#(isNeList(V1), isList(V2))) (active#(__(X1, X2)) -> active#(X1), active#(isNeList(V)) -> isQid#(V)) (active#(__(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> and#(active(X1), X2)) (active#(__(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> active#(X1)) (active#(__(X1, X2)) -> active#(X1), active#(__(__(X, Y), Z)) -> __#(Y, Z)) (active#(__(X1, X2)) -> active#(X1), active#(__(__(X, Y), Z)) -> __#(X, __(Y, Z))) (active#(__(X1, X2)) -> active#(X1), active#(__(X1, X2)) -> active#(X2)) (active#(__(X1, X2)) -> active#(X1), active#(__(X1, X2)) -> active#(X1)) (active#(__(X1, X2)) -> active#(X1), active#(__(X1, X2)) -> __#(active(X1), X2)) (active#(__(X1, X2)) -> active#(X1), active#(__(X1, X2)) -> __#(X1, active(X2))) (proper#(__(X1, X2)) -> proper#(X1), proper#(isPal(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isPal(X)) -> isPal#(proper(X))) (proper#(__(X1, X2)) -> proper#(X1), proper#(isNePal(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isNePal(X)) -> isNePal#(proper(X))) (proper#(__(X1, X2)) -> proper#(X1), proper#(isQid(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isQid(X)) -> isQid#(proper(X))) (proper#(__(X1, X2)) -> proper#(X1), proper#(isList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isList(X)) -> isList#(proper(X))) (proper#(__(X1, X2)) -> proper#(X1), proper#(isNeList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isNeList(X)) -> isNeList#(proper(X))) (proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2))) (proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> __#(proper(X1), proper(X2))) (active#(__(X1, X2)) -> __#(X1, active(X2)), __#(ok(X1), ok(X2)) -> __#(X1, X2)) (active#(__(X1, X2)) -> __#(X1, active(X2)), __#(mark(X1), X2) -> __#(X1, X2)) (active#(__(X1, X2)) -> __#(X1, active(X2)), __#(X1, mark(X2)) -> __#(X1, X2)) (active#(isNeList(__(V1, V2))) -> and#(isList(V1), isNeList(V2)), and#(ok(X1), ok(X2)) -> and#(X1, X2)) (active#(isNeList(__(V1, V2))) -> and#(isList(V1), isNeList(V2)), and#(mark(X1), X2) -> and#(X1, X2)) (active#(isNePal(__(I, __(P, I)))) -> and#(isQid(I), isPal(P)), and#(ok(X1), ok(X2)) -> and#(X1, X2)) (active#(isNePal(__(I, __(P, I)))) -> and#(isQid(I), isPal(P)), 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#(and(X1, X2)) -> and#(proper(X1), proper(X2)), and#(mark(X1), X2) -> and#(X1, X2)) (active#(isNeList(__(V1, V2))) -> isNeList#(V2), isNeList#(ok(X)) -> isNeList#(X)) (active#(isList(__(V1, V2))) -> isList#(V2), isList#(ok(X)) -> isList#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> isPal#(proper(X))) (proper#(__(X1, X2)) -> proper#(X2), proper#(isNePal(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isNePal(X)) -> isNePal#(proper(X))) (proper#(__(X1, X2)) -> proper#(X2), proper#(isQid(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isQid(X)) -> isQid#(proper(X))) (proper#(__(X1, X2)) -> proper#(X2), proper#(isList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isList(X)) -> isList#(proper(X))) (proper#(__(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> isNeList#(proper(X))) (proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2))) (proper#(__(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> __#(proper(X1), proper(X2))) (active#(__(__(X, Y), Z)) -> __#(X, __(Y, Z)), __#(ok(X1), ok(X2)) -> __#(X1, X2)) (active#(__(__(X, Y), Z)) -> __#(X, __(Y, Z)), __#(mark(X1), X2) -> __#(X1, X2)) (active#(__(__(X, Y), Z)) -> __#(X, __(Y, Z)), __#(X1, mark(X2)) -> __#(X1, X2)) (active#(__(X1, X2)) -> __#(active(X1), X2), __#(ok(X1), ok(X2)) -> __#(X1, X2)) (active#(__(X1, X2)) -> __#(active(X1), X2), __#(mark(X1), X2) -> __#(X1, X2)) (active#(__(X1, X2)) -> __#(active(X1), X2), __#(X1, mark(X2)) -> __#(X1, X2)) (active#(isNeList(V)) -> isQid#(V), isQid#(ok(X)) -> isQid#(X)) (active#(isNePal(V)) -> isQid#(V), isQid#(ok(X)) -> isQid#(X)) (proper#(isNeList(X)) -> isNeList#(proper(X)), isNeList#(ok(X)) -> isNeList#(X)) (proper#(isQid(X)) -> isQid#(proper(X)), isQid#(ok(X)) -> isQid#(X)) (proper#(isPal(X)) -> isPal#(proper(X)), isPal#(ok(X)) -> isPal#(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)) (__#(X1, mark(X2)) -> __#(X1, X2), __#(ok(X1), ok(X2)) -> __#(X1, X2)) (__#(X1, mark(X2)) -> __#(X1, X2), __#(mark(X1), X2) -> __#(X1, X2)) (__#(X1, mark(X2)) -> __#(X1, X2), __#(X1, mark(X2)) -> __#(X1, X2)) (__#(ok(X1), ok(X2)) -> __#(X1, X2), __#(ok(X1), ok(X2)) -> __#(X1, X2)) (__#(ok(X1), ok(X2)) -> __#(X1, X2), __#(mark(X1), X2) -> __#(X1, X2)) (__#(ok(X1), ok(X2)) -> __#(X1, X2), __#(X1, mark(X2)) -> __#(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)) (isList#(ok(X)) -> isList#(X), isList#(ok(X)) -> isList#(X)) (isNePal#(ok(X)) -> isNePal#(X), isNePal#(ok(X)) -> isNePal#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isPal(X)) -> isPal#(proper(X))) (proper#(isNeList(X)) -> proper#(X), proper#(isNePal(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isNePal(X)) -> isNePal#(proper(X))) (proper#(isNeList(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isQid(X)) -> isQid#(proper(X))) (proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> isList#(proper(X))) (proper#(isNeList(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isNeList(X)) -> isNeList#(proper(X))) (proper#(isNeList(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isNeList(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1)) (proper#(isNeList(X)) -> proper#(X), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2))) (proper#(isNeList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isNeList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isNeList(X)) -> proper#(X), proper#(__(X1, X2)) -> __#(proper(X1), proper(X2))) (proper#(isQid(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isQid(X)) -> proper#(X), proper#(isPal(X)) -> isPal#(proper(X))) (proper#(isQid(X)) -> proper#(X), proper#(isNePal(X)) -> proper#(X)) (proper#(isQid(X)) -> proper#(X), proper#(isNePal(X)) -> isNePal#(proper(X))) (proper#(isQid(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X)) (proper#(isQid(X)) -> proper#(X), proper#(isQid(X)) -> isQid#(proper(X))) (proper#(isQid(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isQid(X)) -> proper#(X), proper#(isList(X)) -> isList#(proper(X))) (proper#(isQid(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isQid(X)) -> proper#(X), proper#(isNeList(X)) -> isNeList#(proper(X))) (proper#(isQid(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isQid(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1)) (proper#(isQid(X)) -> proper#(X), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2))) (proper#(isQid(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isQid(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isQid(X)) -> proper#(X), proper#(__(X1, X2)) -> __#(proper(X1), proper(X2))) (proper#(isPal(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isPal(X)) -> isPal#(proper(X))) (proper#(isPal(X)) -> proper#(X), proper#(isNePal(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isNePal(X)) -> isNePal#(proper(X))) (proper#(isPal(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isQid(X)) -> isQid#(proper(X))) (proper#(isPal(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isList(X)) -> isList#(proper(X))) (proper#(isPal(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isNeList(X)) -> isNeList#(proper(X))) (proper#(isPal(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isPal(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1)) (proper#(isPal(X)) -> proper#(X), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2))) (proper#(isPal(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isPal(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isPal(X)) -> proper#(X), proper#(__(X1, X2)) -> __#(proper(X1), proper(X2))) (top#(ok(X)) -> active#(X), active#(isPal(V)) -> isNePal#(V)) (top#(ok(X)) -> active#(X), active#(isNePal(__(I, __(P, I)))) -> isPal#(P)) (top#(ok(X)) -> active#(X), active#(isNePal(__(I, __(P, I)))) -> isQid#(I)) (top#(ok(X)) -> active#(X), active#(isNePal(__(I, __(P, I)))) -> and#(isQid(I), isPal(P))) (top#(ok(X)) -> active#(X), active#(isNePal(V)) -> isQid#(V)) (top#(ok(X)) -> active#(X), active#(isList(__(V1, V2))) -> isList#(V2)) (top#(ok(X)) -> active#(X), active#(isList(__(V1, V2))) -> isList#(V1)) (top#(ok(X)) -> active#(X), active#(isList(__(V1, V2))) -> and#(isList(V1), isList(V2))) (top#(ok(X)) -> active#(X), active#(isList(V)) -> isNeList#(V)) (top#(ok(X)) -> active#(X), active#(isNeList(__(V1, V2))) -> isList#(V2)) (top#(ok(X)) -> active#(X), active#(isNeList(__(V1, V2))) -> isList#(V1)) (top#(ok(X)) -> active#(X), active#(isNeList(__(V1, V2))) -> isNeList#(V2)) (top#(ok(X)) -> active#(X), active#(isNeList(__(V1, V2))) -> isNeList#(V1)) (top#(ok(X)) -> active#(X), active#(isNeList(__(V1, V2))) -> and#(isList(V1), isNeList(V2))) (top#(ok(X)) -> active#(X), active#(isNeList(__(V1, V2))) -> and#(isNeList(V1), isList(V2))) (top#(ok(X)) -> active#(X), active#(isNeList(V)) -> isQid#(V)) (top#(ok(X)) -> active#(X), active#(and(X1, X2)) -> and#(active(X1), X2)) (top#(ok(X)) -> active#(X), active#(and(X1, X2)) -> active#(X1)) (top#(ok(X)) -> active#(X), active#(__(__(X, Y), Z)) -> __#(Y, Z)) (top#(ok(X)) -> active#(X), active#(__(__(X, Y), Z)) -> __#(X, __(Y, Z))) (top#(ok(X)) -> active#(X), active#(__(X1, X2)) -> active#(X2)) (top#(ok(X)) -> active#(X), active#(__(X1, X2)) -> active#(X1)) (top#(ok(X)) -> active#(X), active#(__(X1, X2)) -> __#(active(X1), X2)) (top#(ok(X)) -> active#(X), active#(__(X1, X2)) -> __#(X1, active(X2))) (top#(mark(X)) -> proper#(X), proper#(__(X1, X2)) -> __#(proper(X1), proper(X2))) (top#(mark(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (top#(mark(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (top#(mark(X)) -> proper#(X), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2))) (top#(mark(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1)) (top#(mark(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (top#(mark(X)) -> proper#(X), proper#(isNeList(X)) -> isNeList#(proper(X))) (top#(mark(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (top#(mark(X)) -> proper#(X), proper#(isList(X)) -> isList#(proper(X))) (top#(mark(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (top#(mark(X)) -> proper#(X), proper#(isQid(X)) -> isQid#(proper(X))) (top#(mark(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X)) (top#(mark(X)) -> proper#(X), proper#(isNePal(X)) -> isNePal#(proper(X))) (top#(mark(X)) -> proper#(X), proper#(isNePal(X)) -> proper#(X)) (top#(mark(X)) -> proper#(X), proper#(isPal(X)) -> isPal#(proper(X))) (top#(mark(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isNePal(X)) -> proper#(X), proper#(__(X1, X2)) -> __#(proper(X1), proper(X2))) (proper#(isNePal(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isNePal(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isNePal(X)) -> proper#(X), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2))) (proper#(isNePal(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1)) (proper#(isNePal(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isNePal(X)) -> proper#(X), proper#(isNeList(X)) -> isNeList#(proper(X))) (proper#(isNePal(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isNePal(X)) -> proper#(X), proper#(isList(X)) -> isList#(proper(X))) (proper#(isNePal(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isNePal(X)) -> proper#(X), proper#(isQid(X)) -> isQid#(proper(X))) (proper#(isNePal(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X)) (proper#(isNePal(X)) -> proper#(X), proper#(isNePal(X)) -> isNePal#(proper(X))) (proper#(isNePal(X)) -> proper#(X), proper#(isNePal(X)) -> proper#(X)) (proper#(isNePal(X)) -> proper#(X), proper#(isPal(X)) -> isPal#(proper(X))) (proper#(isNePal(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(__(X1, X2)) -> __#(proper(X1), proper(X2))) (proper#(isList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isList(X)) -> proper#(X), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2))) (proper#(isList(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1)) (proper#(isList(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isList(X)) -> proper#(X), proper#(isNeList(X)) -> isNeList#(proper(X))) (proper#(isList(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(isList(X)) -> isList#(proper(X))) (proper#(isList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(isQid(X)) -> isQid#(proper(X))) (proper#(isList(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(isNePal(X)) -> isNePal#(proper(X))) (proper#(isList(X)) -> proper#(X), proper#(isNePal(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(isPal(X)) -> isPal#(proper(X))) (proper#(isList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (isPal#(ok(X)) -> isPal#(X), isPal#(ok(X)) -> isPal#(X)) (isQid#(ok(X)) -> isQid#(X), isQid#(ok(X)) -> isQid#(X)) (isNeList#(ok(X)) -> isNeList#(X), isNeList#(ok(X)) -> isNeList#(X)) (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)) (__#(mark(X1), X2) -> __#(X1, X2), __#(X1, mark(X2)) -> __#(X1, X2)) (__#(mark(X1), X2) -> __#(X1, X2), __#(mark(X1), X2) -> __#(X1, X2)) (__#(mark(X1), X2) -> __#(X1, X2), __#(ok(X1), ok(X2)) -> __#(X1, X2)) (active#(isNePal(__(I, __(P, I)))) -> isPal#(P), isPal#(ok(X)) -> isPal#(X)) (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#(isNePal(X)) -> isNePal#(proper(X)), isNePal#(ok(X)) -> isNePal#(X)) (proper#(isList(X)) -> isList#(proper(X)), isList#(ok(X)) -> isList#(X)) (active#(isPal(V)) -> isNePal#(V), isNePal#(ok(X)) -> isNePal#(X)) (active#(isList(V)) -> isNeList#(V), isNeList#(ok(X)) -> isNeList#(X)) (active#(and(X1, X2)) -> and#(active(X1), X2), and#(mark(X1), X2) -> and#(X1, X2)) (active#(and(X1, X2)) -> and#(active(X1), X2), and#(ok(X1), ok(X2)) -> and#(X1, X2)) (active#(isNePal(__(I, __(P, I)))) -> isQid#(I), isQid#(ok(X)) -> isQid#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> __#(proper(X1), proper(X2))) (proper#(and(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X1)) (proper#(and(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X2)) (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#(isNeList(X)) -> isNeList#(proper(X))) (proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isList(X)) -> isList#(proper(X))) (proper#(and(X1, X2)) -> proper#(X2), proper#(isList(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isQid(X)) -> isQid#(proper(X))) (proper#(and(X1, X2)) -> proper#(X2), proper#(isQid(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isNePal(X)) -> isNePal#(proper(X))) (proper#(and(X1, X2)) -> proper#(X2), proper#(isNePal(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> isPal#(proper(X))) (proper#(and(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> proper#(X)) (active#(__(X1, X2)) -> active#(X2), active#(__(X1, X2)) -> __#(X1, active(X2))) (active#(__(X1, X2)) -> active#(X2), active#(__(X1, X2)) -> __#(active(X1), X2)) (active#(__(X1, X2)) -> active#(X2), active#(__(X1, X2)) -> active#(X1)) (active#(__(X1, X2)) -> active#(X2), active#(__(X1, X2)) -> active#(X2)) (active#(__(X1, X2)) -> active#(X2), active#(__(__(X, Y), Z)) -> __#(X, __(Y, Z))) (active#(__(X1, X2)) -> active#(X2), active#(__(__(X, Y), Z)) -> __#(Y, Z)) (active#(__(X1, X2)) -> active#(X2), active#(and(X1, X2)) -> active#(X1)) (active#(__(X1, X2)) -> active#(X2), active#(and(X1, X2)) -> and#(active(X1), X2)) (active#(__(X1, X2)) -> active#(X2), active#(isNeList(V)) -> isQid#(V)) (active#(__(X1, X2)) -> active#(X2), active#(isNeList(__(V1, V2))) -> and#(isNeList(V1), isList(V2))) (active#(__(X1, X2)) -> active#(X2), active#(isNeList(__(V1, V2))) -> and#(isList(V1), isNeList(V2))) (active#(__(X1, X2)) -> active#(X2), active#(isNeList(__(V1, V2))) -> isNeList#(V1)) (active#(__(X1, X2)) -> active#(X2), active#(isNeList(__(V1, V2))) -> isNeList#(V2)) (active#(__(X1, X2)) -> active#(X2), active#(isNeList(__(V1, V2))) -> isList#(V1)) (active#(__(X1, X2)) -> active#(X2), active#(isNeList(__(V1, V2))) -> isList#(V2)) (active#(__(X1, X2)) -> active#(X2), active#(isList(V)) -> isNeList#(V)) (active#(__(X1, X2)) -> active#(X2), active#(isList(__(V1, V2))) -> and#(isList(V1), isList(V2))) (active#(__(X1, X2)) -> active#(X2), active#(isList(__(V1, V2))) -> isList#(V1)) (active#(__(X1, X2)) -> active#(X2), active#(isList(__(V1, V2))) -> isList#(V2)) (active#(__(X1, X2)) -> active#(X2), active#(isNePal(V)) -> isQid#(V)) (active#(__(X1, X2)) -> active#(X2), active#(isNePal(__(I, __(P, I)))) -> and#(isQid(I), isPal(P))) (active#(__(X1, X2)) -> active#(X2), active#(isNePal(__(I, __(P, I)))) -> isQid#(I)) (active#(__(X1, X2)) -> active#(X2), active#(isNePal(__(I, __(P, I)))) -> isPal#(P)) (active#(__(X1, X2)) -> active#(X2), active#(isPal(V)) -> isNePal#(V)) (active#(isNeList(__(V1, V2))) -> isList#(V2), isList#(ok(X)) -> isList#(X)) (active#(__(__(X, Y), Z)) -> __#(Y, Z), __#(X1, mark(X2)) -> __#(X1, X2)) (active#(__(__(X, Y), Z)) -> __#(Y, Z), __#(mark(X1), X2) -> __#(X1, X2)) (active#(__(__(X, Y), Z)) -> __#(Y, Z), __#(ok(X1), ok(X2)) -> __#(X1, X2)) (proper#(__(X1, X2)) -> __#(proper(X1), proper(X2)), __#(X1, mark(X2)) -> __#(X1, X2)) (proper#(__(X1, X2)) -> __#(proper(X1), proper(X2)), __#(mark(X1), X2) -> __#(X1, X2)) (proper#(__(X1, X2)) -> __#(proper(X1), proper(X2)), __#(ok(X1), ok(X2)) -> __#(X1, X2)) (active#(isList(__(V1, V2))) -> and#(isList(V1), isList(V2)), and#(mark(X1), X2) -> and#(X1, X2)) (active#(isList(__(V1, V2))) -> and#(isList(V1), isList(V2)), and#(ok(X1), ok(X2)) -> and#(X1, X2)) (active#(isNeList(__(V1, V2))) -> and#(isNeList(V1), isList(V2)), and#(mark(X1), X2) -> and#(X1, X2)) (active#(isNeList(__(V1, V2))) -> and#(isNeList(V1), isList(V2)), and#(ok(X1), ok(X2)) -> and#(X1, X2)) (proper#(and(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> __#(proper(X1), proper(X2))) (proper#(and(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X1)) (proper#(and(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2)) (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2))) (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#(isNeList(X)) -> isNeList#(proper(X))) (proper#(and(X1, X2)) -> proper#(X1), proper#(isNeList(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X1), proper#(isList(X)) -> isList#(proper(X))) (proper#(and(X1, X2)) -> proper#(X1), proper#(isList(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X1), proper#(isQid(X)) -> isQid#(proper(X))) (proper#(and(X1, X2)) -> proper#(X1), proper#(isQid(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X1), proper#(isNePal(X)) -> isNePal#(proper(X))) (proper#(and(X1, X2)) -> proper#(X1), proper#(isNePal(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X1), proper#(isPal(X)) -> isPal#(proper(X))) (proper#(and(X1, X2)) -> proper#(X1), proper#(isPal(X)) -> proper#(X)) (active#(and(X1, X2)) -> active#(X1), active#(__(X1, X2)) -> __#(X1, active(X2))) (active#(and(X1, X2)) -> active#(X1), active#(__(X1, X2)) -> __#(active(X1), X2)) (active#(and(X1, X2)) -> active#(X1), active#(__(X1, X2)) -> active#(X1)) (active#(and(X1, X2)) -> active#(X1), active#(__(X1, X2)) -> active#(X2)) (active#(and(X1, X2)) -> active#(X1), active#(__(__(X, Y), Z)) -> __#(X, __(Y, Z))) (active#(and(X1, X2)) -> active#(X1), active#(__(__(X, Y), Z)) -> __#(Y, Z)) (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#(isNeList(V)) -> isQid#(V)) (active#(and(X1, X2)) -> active#(X1), active#(isNeList(__(V1, V2))) -> and#(isNeList(V1), isList(V2))) (active#(and(X1, X2)) -> active#(X1), active#(isNeList(__(V1, V2))) -> and#(isList(V1), isNeList(V2))) (active#(and(X1, X2)) -> active#(X1), active#(isNeList(__(V1, V2))) -> isNeList#(V1)) (active#(and(X1, X2)) -> active#(X1), active#(isNeList(__(V1, V2))) -> isNeList#(V2)) (active#(and(X1, X2)) -> active#(X1), active#(isNeList(__(V1, V2))) -> isList#(V1)) (active#(and(X1, X2)) -> active#(X1), active#(isNeList(__(V1, V2))) -> isList#(V2)) (active#(and(X1, X2)) -> active#(X1), active#(isList(V)) -> isNeList#(V)) (active#(and(X1, X2)) -> active#(X1), active#(isList(__(V1, V2))) -> and#(isList(V1), isList(V2))) (active#(and(X1, X2)) -> active#(X1), active#(isList(__(V1, V2))) -> isList#(V1)) (active#(and(X1, X2)) -> active#(X1), active#(isList(__(V1, V2))) -> isList#(V2)) (active#(and(X1, X2)) -> active#(X1), active#(isNePal(V)) -> isQid#(V)) (active#(and(X1, X2)) -> active#(X1), active#(isNePal(__(I, __(P, I)))) -> and#(isQid(I), isPal(P))) (active#(and(X1, X2)) -> active#(X1), active#(isNePal(__(I, __(P, I)))) -> isQid#(I)) (active#(and(X1, X2)) -> active#(X1), active#(isNePal(__(I, __(P, I)))) -> isPal#(P)) (active#(and(X1, X2)) -> active#(X1), active#(isPal(V)) -> isNePal#(V)) (active#(isList(__(V1, V2))) -> isList#(V1), isList#(ok(X)) -> isList#(X)) (active#(isNeList(__(V1, V2))) -> isNeList#(V1), isNeList#(ok(X)) -> isNeList#(X)) } SCCS: Scc: {top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X))} Scc: { proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X), proper#(isNePal(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} Scc: {isPal#(ok(X)) -> isPal#(X)} Scc: {isNePal#(ok(X)) -> isNePal#(X)} Scc: {isQid#(ok(X)) -> isQid#(X)} Scc: {isList#(ok(X)) -> isList#(X)} Scc: {isNeList#(ok(X)) -> isNeList#(X)} Scc: { and#(mark(X1), X2) -> and#(X1, X2), and#(ok(X1), ok(X2)) -> and#(X1, X2)} Scc: { active#(__(X1, X2)) -> active#(X1), active#(__(X1, X2)) -> active#(X2), active#(and(X1, X2)) -> active#(X1)} Scc: { __#(X1, mark(X2)) -> __#(X1, X2), __#(mark(X1), X2) -> __#(X1, X2), __#(ok(X1), ok(X2)) -> __#(X1, X2)} SCC: Strict: {top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X))} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} Fail SCC: Strict: { proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X), proper#(isNePal(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} EDG: {(proper#(and(X1, X2)) -> proper#(X1), proper#(isPal(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X1), proper#(isQid(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X1), proper#(isList(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X1), proper#(isNeList(X)) -> proper#(X)) (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#(__(X1, X2)) -> proper#(X2)) (proper#(and(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isList(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1)) (proper#(isList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isPal(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isPal(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1)) (proper#(isPal(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isPal(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isQid(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isList(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X)) (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#(and(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X2)) (proper#(and(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isQid(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> proper#(X)) (proper#(isQid(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isQid(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isQid(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1)) (proper#(isQid(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isQid(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isQid(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isQid(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X)) (proper#(isQid(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isNeList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isNeList(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1)) (proper#(isNeList(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isNeList(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isNeList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isQid(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isPal(X)) -> proper#(X))} SCCS: Scc: { proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} SCC: Strict: { proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} EDG: {(proper#(isNeList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isNeList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isNeList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isQid(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isQid(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X)) (proper#(isQid(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isQid(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isQid(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isQid(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isQid(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isQid(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X1)) (proper#(and(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X1)) (proper#(and(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X2)) (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isList(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isQid(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isPal(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isPal(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isPal(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isList(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isList(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isNeList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isQid(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isPal(X)) -> proper#(X))} SCCS: Scc: { proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} SCC: Strict: { proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X), proper#(isQid(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} EDG: {(proper#(and(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isList(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2)) (proper#(and(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X2)) (proper#(and(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isPal(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isNeList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isPal(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isPal(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isPal(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isPal(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isNeList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X2)) (proper#(isNeList(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isNeList(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> proper#(X))} SCCS: Scc: { proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} SCC: Strict: { proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} EDG: {(proper#(isList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isList(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isPal(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isNeList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X1)) (proper#(and(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X1)) (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isList(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isPal(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isPal(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isNeList(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isNeList(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X))} SCCS: Scc: { proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} SCC: Strict: { proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} EDG: {(proper#(isNeList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isNeList(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isNeList(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2)) (proper#(and(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isPal(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isPal(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isPal(X)) -> proper#(X), proper#(isNeList(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isNeList(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isPal(X)) -> proper#(X))} SCCS: Scc: { proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} SCC: Strict: { proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2), proper#(isNeList(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> proper#(X)} EDG: {(proper#(__(X1, X2)) -> proper#(X1), proper#(isPal(X)) -> proper#(X)) (proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2)) (proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isPal(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(isPal(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2)) (proper#(isPal(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(and(X1, X2)) -> proper#(X2), proper#(__(X1, X2)) -> proper#(X1)) (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2)) (proper#(and(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> proper#(X))} SCCS: Scc: { proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> proper#(X)} SCC: Strict: { proper#(__(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2), proper#(isPal(X)) -> proper#(X)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(__(X1, X2)) -> proper#(X1), proper#(isPal(X)) -> proper#(X)} EDG: {(proper#(isPal(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X)) (proper#(isPal(X)) -> proper#(X), proper#(__(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X1), proper#(__(X1, X2)) -> proper#(X1)) (proper#(__(X1, X2)) -> proper#(X1), proper#(isPal(X)) -> proper#(X))} SCCS: Scc: {proper#(__(X1, X2)) -> proper#(X1), proper#(isPal(X)) -> proper#(X)} SCC: Strict: {proper#(__(X1, X2)) -> proper#(X1), proper#(isPal(X)) -> proper#(X)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(isPal(X)) -> proper#(X)} EDG: {(proper#(isPal(X)) -> proper#(X), proper#(isPal(X)) -> proper#(X))} SCCS: Scc: {proper#(isPal(X)) -> proper#(X)} SCC: Strict: {proper#(isPal(X)) -> proper#(X)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {} Qed SCC: Strict: {isPal#(ok(X)) -> isPal#(X)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(isPal#) = 0 Strict: {} Qed SCC: Strict: {isNePal#(ok(X)) -> isNePal#(X)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(isNePal#) = 0 Strict: {} Qed SCC: Strict: {isQid#(ok(X)) -> isQid#(X)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(isQid#) = 0 Strict: {} Qed SCC: Strict: {isList#(ok(X)) -> isList#(X)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(isList#) = 0 Strict: {} Qed SCC: Strict: {isNeList#(ok(X)) -> isNeList#(X)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(isNeList#) = 0 Strict: {} Qed SCC: Strict: { and#(mark(X1), X2) -> and#(X1, X2), and#(ok(X1), ok(X2)) -> and#(X1, X2)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(and#) = 0 Strict: {and#(ok(X1), ok(X2)) -> and#(X1, X2)} EDG: {(and#(ok(X1), ok(X2)) -> and#(X1, X2), and#(ok(X1), ok(X2)) -> and#(X1, X2))} SCCS: Scc: {and#(ok(X1), ok(X2)) -> and#(X1, X2)} SCC: Strict: {and#(ok(X1), ok(X2)) -> and#(X1, X2)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(and#) = 0 Strict: {} Qed SCC: Strict: { active#(__(X1, X2)) -> active#(X1), active#(__(X1, X2)) -> active#(X2), active#(and(X1, X2)) -> active#(X1)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: { active#(__(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> active#(X1)} EDG: {(active#(and(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> active#(X1)) (active#(and(X1, X2)) -> active#(X1), active#(__(X1, X2)) -> active#(X1)) (active#(__(X1, X2)) -> active#(X1), active#(__(X1, X2)) -> active#(X1)) (active#(__(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> active#(X1))} SCCS: Scc: { active#(__(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> active#(X1)} SCC: Strict: { active#(__(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> active#(X1)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), 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)} EDG: {(active#(and(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> active#(X1))} SCCS: Scc: {active#(and(X1, X2)) -> active#(X1)} SCC: Strict: {active#(and(X1, X2)) -> active#(X1)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: {} Qed SCC: Strict: { __#(X1, mark(X2)) -> __#(X1, X2), __#(mark(X1), X2) -> __#(X1, X2), __#(ok(X1), ok(X2)) -> __#(X1, X2)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(__#) = 0 Strict: {__#(X1, mark(X2)) -> __#(X1, X2), __#(mark(X1), X2) -> __#(X1, X2)} EDG: {(__#(mark(X1), X2) -> __#(X1, X2), __#(mark(X1), X2) -> __#(X1, X2)) (__#(mark(X1), X2) -> __#(X1, X2), __#(X1, mark(X2)) -> __#(X1, X2)) (__#(X1, mark(X2)) -> __#(X1, X2), __#(X1, mark(X2)) -> __#(X1, X2)) (__#(X1, mark(X2)) -> __#(X1, X2), __#(mark(X1), X2) -> __#(X1, X2))} SCCS: Scc: {__#(X1, mark(X2)) -> __#(X1, X2), __#(mark(X1), X2) -> __#(X1, X2)} SCC: Strict: {__#(X1, mark(X2)) -> __#(X1, X2), __#(mark(X1), X2) -> __#(X1, X2)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(__#) = 0 Strict: {__#(X1, mark(X2)) -> __#(X1, X2)} EDG: {(__#(X1, mark(X2)) -> __#(X1, X2), __#(X1, mark(X2)) -> __#(X1, X2))} SCCS: Scc: {__#(X1, mark(X2)) -> __#(X1, X2)} SCC: Strict: {__#(X1, mark(X2)) -> __#(X1, X2)} Weak: { __(X1, mark(X2)) -> mark(__(X1, X2)), __(mark(X1), X2) -> mark(__(X1, X2)), __(ok(X1), ok(X2)) -> ok(__(X1, X2)), active(__(X, nil())) -> mark(X), active(__(X1, X2)) -> __(X1, active(X2)), active(__(X1, X2)) -> __(active(X1), X2), active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))), active(__(nil(), X)) -> mark(X), active(and(X1, X2)) -> and(active(X1), X2), active(and(tt(), X)) -> mark(X), active(isNeList(V)) -> mark(isQid(V)), active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))), active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))), active(isList(V)) -> mark(isNeList(V)), active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))), active(isList(nil())) -> mark(tt()), active(isQid(a())) -> mark(tt()), active(isQid(e())) -> mark(tt()), active(isQid(i())) -> mark(tt()), active(isQid(o())) -> mark(tt()), active(isQid(u())) -> mark(tt()), active(isNePal(V)) -> mark(isQid(V)), active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))), active(isPal(V)) -> mark(isNePal(V)), active(isPal(nil())) -> mark(tt()), and(mark(X1), X2) -> mark(and(X1, X2)), and(ok(X1), ok(X2)) -> ok(and(X1, X2)), isNeList(ok(X)) -> ok(isNeList(X)), isList(ok(X)) -> ok(isList(X)), isQid(ok(X)) -> ok(isQid(X)), isNePal(ok(X)) -> ok(isNePal(X)), isPal(ok(X)) -> ok(isPal(X)), proper(__(X1, X2)) -> __(proper(X1), proper(X2)), proper(nil()) -> ok(nil()), proper(and(X1, X2)) -> and(proper(X1), proper(X2)), proper(tt()) -> ok(tt()), proper(isNeList(X)) -> isNeList(proper(X)), proper(isList(X)) -> isList(proper(X)), proper(isQid(X)) -> isQid(proper(X)), proper(isNePal(X)) -> isNePal(proper(X)), proper(isPal(X)) -> isPal(proper(X)), proper(a()) -> ok(a()), proper(e()) -> ok(e()), proper(i()) -> ok(i()), proper(o()) -> ok(o()), proper(u()) -> ok(u()), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(__#) = 1 Strict: {} Qed