MAYBE Time: 0.410950 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} DP: DP: { __#(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# U12 X -> active# X, active# U12 X -> U12# active X, active# U11 X -> active# X, active# U11 X -> U11# active X, active# U11 tt() -> U12# tt(), active# isNePal X -> active# X, active# isNePal X -> isNePal# active X, active# isNePal __(I, __(P, I)) -> U11# tt(), U12# mark X -> U12# X, U12# ok X -> U12# X, U11# mark X -> U11# X, U11# ok X -> U11# X, isNePal# mark X -> isNePal# X, isNePal# ok X -> isNePal# X, proper# __(X1, X2) -> __#(proper X1, proper X2), proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2, proper# U12 X -> U12# proper X, proper# U12 X -> proper# X, proper# U11 X -> U11# proper X, proper# U11 X -> proper# X, proper# isNePal X -> isNePal# proper X, proper# isNePal 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} 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} UR: { __(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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X} EDG: { (active# U12 X -> active# X, active# isNePal __(I, __(P, I)) -> U11# tt()) (active# U12 X -> active# X, active# isNePal X -> isNePal# active X) (active# U12 X -> active# X, active# isNePal X -> active# X) (active# U12 X -> active# X, active# U11 tt() -> U12# tt()) (active# U12 X -> active# X, active# U11 X -> U11# active X) (active# U12 X -> active# X, active# U11 X -> active# X) (active# U12 X -> active# X, active# U12 X -> U12# active X) (active# U12 X -> active# X, active# U12 X -> active# X) (active# U12 X -> active# X, active# __(__(X, Y), Z) -> __#(Y, Z)) (active# U12 X -> active# X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z))) (active# U12 X -> active# X, active# __(X1, X2) -> active# X2) (active# U12 X -> active# X, active# __(X1, X2) -> active# X1) (active# U12 X -> active# X, active# __(X1, X2) -> __#(active X1, X2)) (active# U12 X -> active# X, active# __(X1, X2) -> __#(X1, active X2)) (active# isNePal X -> active# X, active# isNePal __(I, __(P, I)) -> U11# tt()) (active# isNePal X -> active# X, active# isNePal X -> isNePal# active X) (active# isNePal X -> active# X, active# isNePal X -> active# X) (active# isNePal X -> active# X, active# U11 tt() -> U12# tt()) (active# isNePal X -> active# X, active# U11 X -> U11# active X) (active# isNePal X -> active# X, active# U11 X -> active# X) (active# isNePal X -> active# X, active# U12 X -> U12# active X) (active# isNePal X -> active# X, active# U12 X -> active# X) (active# isNePal X -> active# X, active# __(__(X, Y), Z) -> __#(Y, Z)) (active# isNePal X -> active# X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z))) (active# isNePal X -> active# X, active# __(X1, X2) -> active# X2) (active# isNePal X -> active# X, active# __(X1, X2) -> active# X1) (active# isNePal X -> active# X, active# __(X1, X2) -> __#(active X1, X2)) (active# isNePal X -> active# X, active# __(X1, X2) -> __#(X1, active X2)) (U12# ok X -> U12# X, U12# ok X -> U12# X) (U12# ok X -> U12# X, U12# mark X -> U12# X) (U11# ok X -> U11# X, U11# ok X -> U11# X) (U11# ok X -> U11# X, U11# mark X -> U11# X) (isNePal# ok X -> isNePal# X, isNePal# ok X -> isNePal# X) (isNePal# ok X -> isNePal# X, isNePal# mark X -> isNePal# X) (proper# U11 X -> proper# X, proper# isNePal X -> proper# X) (proper# U11 X -> proper# X, proper# isNePal X -> isNePal# proper X) (proper# U11 X -> proper# X, proper# U11 X -> proper# X) (proper# U11 X -> proper# X, proper# U11 X -> U11# proper X) (proper# U11 X -> proper# X, proper# U12 X -> proper# X) (proper# U11 X -> proper# X, proper# U12 X -> U12# proper X) (proper# U11 X -> proper# X, proper# __(X1, X2) -> proper# X2) (proper# U11 X -> proper# X, proper# __(X1, X2) -> proper# X1) (proper# U11 X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2)) (top# mark X -> proper# X, proper# isNePal X -> proper# X) (top# mark X -> proper# X, proper# isNePal X -> isNePal# proper X) (top# mark X -> proper# X, proper# U11 X -> proper# X) (top# mark X -> proper# X, proper# U11 X -> U11# proper X) (top# mark X -> proper# X, proper# U12 X -> proper# X) (top# mark X -> proper# X, proper# U12 X -> U12# proper X) (top# mark X -> proper# X, proper# __(X1, X2) -> proper# X2) (top# mark X -> proper# X, proper# __(X1, X2) -> proper# X1) (top# mark X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper 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# U11 X -> U11# active X, U11# ok X -> U11# X) (active# U11 X -> U11# active X, U11# mark X -> U11# X) (active# isNePal X -> isNePal# active X, isNePal# ok X -> isNePal# X) (active# isNePal X -> isNePal# active X, isNePal# mark X -> isNePal# X) (proper# U12 X -> U12# proper X, U12# ok X -> U12# X) (proper# U12 X -> U12# proper X, U12# mark X -> U12# X) (proper# isNePal X -> isNePal# proper X, isNePal# ok X -> isNePal# X) (proper# isNePal X -> isNePal# proper X, isNePal# mark X -> isNePal# 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) (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# U11 X -> proper# X) (proper# __(X1, X2) -> proper# X2, proper# U11 X -> U11# proper X) (proper# __(X1, X2) -> proper# X2, proper# U12 X -> proper# X) (proper# __(X1, X2) -> proper# X2, proper# U12 X -> U12# proper X) (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)) (proper# __(X1, X2) -> __#(proper X1, proper X2), __#(ok X1, ok X2) -> __#(X1, X2)) (proper# __(X1, X2) -> __#(proper X1, proper X2), __#(mark X1, X2) -> __#(X1, X2)) (proper# __(X1, X2) -> __#(proper X1, proper X2), __#(X1, mark X2) -> __#(X1, X2)) (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# U11 X -> proper# X) (proper# __(X1, X2) -> proper# X1, proper# U11 X -> U11# proper X) (proper# __(X1, X2) -> proper# X1, proper# U12 X -> proper# X) (proper# __(X1, X2) -> proper# X1, proper# U12 X -> U12# proper X) (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)) (__#(mark X1, X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2)) (__#(mark X1, X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2)) (__#(mark X1, X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2)) (active# __(__(X, Y), Z) -> __#(Y, Z), __#(ok X1, ok X2) -> __#(X1, X2)) (active# __(__(X, Y), Z) -> __#(Y, Z), __#(mark X1, X2) -> __#(X1, X2)) (active# __(__(X, Y), Z) -> __#(Y, Z), __#(X1, mark X2) -> __#(X1, X2)) (__#(ok X1, ok X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2)) (__#(ok X1, ok X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2)) (__#(ok X1, ok X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2)) (__#(X1, mark X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2)) (__#(X1, mark X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2)) (__#(X1, mark X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2)) (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> __#(X1, active X2)) (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> __#(active X1, X2)) (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X1) (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2) (active# __(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(X, __(Y, Z))) (active# __(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(Y, Z)) (active# __(X1, X2) -> active# X1, active# U12 X -> active# X) (active# __(X1, X2) -> active# X1, active# U12 X -> U12# active X) (active# __(X1, X2) -> active# X1, active# U11 X -> active# X) (active# __(X1, X2) -> active# X1, active# U11 X -> U11# active X) (active# __(X1, X2) -> active# X1, active# U11 tt() -> U12# tt()) (active# __(X1, X2) -> active# X1, active# isNePal X -> active# X) (active# __(X1, X2) -> active# X1, active# isNePal X -> isNePal# active X) (active# __(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> U11# tt()) (active# __(X1, X2) -> __#(X1, active X2), __#(X1, mark X2) -> __#(X1, X2)) (active# __(X1, X2) -> __#(X1, active X2), __#(mark X1, X2) -> __#(X1, X2)) (active# __(X1, X2) -> __#(X1, active X2), __#(ok X1, ok X2) -> __#(X1, X2)) (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# U12 X -> active# X) (active# __(X1, X2) -> active# X2, active# U12 X -> U12# active X) (active# __(X1, X2) -> active# X2, active# U11 X -> active# X) (active# __(X1, X2) -> active# X2, active# U11 X -> U11# active X) (active# __(X1, X2) -> active# X2, active# U11 tt() -> U12# tt()) (active# __(X1, X2) -> active# X2, active# isNePal X -> active# X) (active# __(X1, X2) -> active# X2, active# isNePal X -> isNePal# active X) (active# __(X1, X2) -> active# X2, active# isNePal __(I, __(P, I)) -> U11# tt()) (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# U11 X -> U11# proper X, U11# mark X -> U11# X) (proper# U11 X -> U11# proper X, U11# ok X -> U11# X) (active# isNePal __(I, __(P, I)) -> U11# tt(), U11# mark X -> U11# X) (active# isNePal __(I, __(P, I)) -> U11# tt(), U11# ok X -> U11# X) (active# U11 tt() -> U12# tt(), U12# mark X -> U12# X) (active# U11 tt() -> U12# tt(), U12# ok X -> U12# X) (active# U12 X -> U12# active X, U12# mark X -> U12# X) (active# U12 X -> U12# active X, U12# ok X -> U12# X) (top# ok X -> active# X, active# __(X1, X2) -> __#(X1, active X2)) (top# ok X -> active# X, active# __(X1, X2) -> __#(active X1, X2)) (top# ok X -> active# X, active# __(X1, X2) -> active# X1) (top# ok X -> active# X, active# __(X1, X2) -> active# X2) (top# ok X -> active# X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z))) (top# ok X -> active# X, active# __(__(X, Y), Z) -> __#(Y, Z)) (top# ok X -> active# X, active# U12 X -> active# X) (top# ok X -> active# X, active# U12 X -> U12# active X) (top# ok X -> active# X, active# U11 X -> active# X) (top# ok X -> active# X, active# U11 X -> U11# active X) (top# ok X -> active# X, active# U11 tt() -> U12# tt()) (top# ok X -> active# X, active# isNePal X -> active# X) (top# ok X -> active# X, active# isNePal X -> isNePal# active X) (top# ok X -> active# X, active# isNePal __(I, __(P, I)) -> U11# tt()) (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# U12 X -> U12# proper X) (proper# isNePal X -> proper# X, proper# U12 X -> proper# X) (proper# isNePal X -> proper# X, proper# U11 X -> U11# proper X) (proper# isNePal X -> proper# X, proper# U11 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# U12 X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2)) (proper# U12 X -> proper# X, proper# __(X1, X2) -> proper# X1) (proper# U12 X -> proper# X, proper# __(X1, X2) -> proper# X2) (proper# U12 X -> proper# X, proper# U12 X -> U12# proper X) (proper# U12 X -> proper# X, proper# U12 X -> proper# X) (proper# U12 X -> proper# X, proper# U11 X -> U11# proper X) (proper# U12 X -> proper# X, proper# U11 X -> proper# X) (proper# U12 X -> proper# X, proper# isNePal X -> isNePal# proper X) (proper# U12 X -> proper# X, proper# isNePal X -> proper# X) (isNePal# mark X -> isNePal# X, isNePal# mark X -> isNePal# X) (isNePal# mark X -> isNePal# X, isNePal# ok X -> isNePal# X) (U11# mark X -> U11# X, U11# mark X -> U11# X) (U11# mark X -> U11# X, U11# ok X -> U11# X) (U12# mark X -> U12# X, U12# mark X -> U12# X) (U12# mark X -> U12# X, U12# ok X -> U12# X) (active# U11 X -> active# X, active# __(X1, X2) -> __#(X1, active X2)) (active# U11 X -> active# X, active# __(X1, X2) -> __#(active X1, X2)) (active# U11 X -> active# X, active# __(X1, X2) -> active# X1) (active# U11 X -> active# X, active# __(X1, X2) -> active# X2) (active# U11 X -> active# X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z))) (active# U11 X -> active# X, active# __(__(X, Y), Z) -> __#(Y, Z)) (active# U11 X -> active# X, active# U12 X -> active# X) (active# U11 X -> active# X, active# U12 X -> U12# active X) (active# U11 X -> active# X, active# U11 X -> active# X) (active# U11 X -> active# X, active# U11 X -> U11# active X) (active# U11 X -> active# X, active# U11 tt() -> U12# tt()) (active# U11 X -> active# X, active# isNePal X -> active# X) (active# U11 X -> active# X, active# isNePal X -> isNePal# active X) (active# U11 X -> active# X, active# isNePal __(I, __(P, I)) -> U11# tt()) (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(X1, mark X2) -> __#(X1, X2)) (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(mark X1, X2) -> __#(X1, X2)) (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(ok X1, ok X2) -> __#(X1, X2)) } STATUS: arrows: 0.847222 SCCS (7): 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# U12 X -> proper# X, proper# U11 X -> proper# X, proper# isNePal X -> proper# X} Scc: {active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2, active# U12 X -> active# X, active# U11 X -> active# X, active# isNePal X -> active# X} Scc: {isNePal# mark X -> isNePal# X, isNePal# ok X -> isNePal# X} Scc: {U11# mark X -> U11# X, U11# ok X -> U11# X} Scc: {U12# mark X -> U12# X, U12# ok X -> U12# X} Scc: { __#(X1, mark X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2)} SCC (2): 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} Fail SCC (5): Strict: {proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2, proper# U12 X -> proper# X, proper# U11 X -> proper# X, proper# isNePal 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = x0 + x1, [mark](x0) = 0, [active](x0) = 0, [U12](x0) = x0, [U11](x0) = x0, [isNePal](x0) = x0 + 1, [proper](x0) = 0, [ok](x0) = x0 + 1, [top](x0) = 0, [nil] = 0, [tt] = 0, [proper#](x0) = x0 Strict: proper# isNePal X -> proper# X 1 + 1X >= 0 + 1X proper# U11 X -> proper# X 0 + 1X >= 0 + 1X proper# U12 X -> proper# X 0 + 1X >= 0 + 1X proper# __(X1, X2) -> proper# X2 0 + 1X1 + 1X2 >= 0 + 1X2 proper# __(X1, X2) -> proper# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 1 + 0X proper U11 X -> U11 proper X 0 + 0X >= 0 + 0X proper tt() -> ok tt() 0 >= 1 proper U12 X -> U12 proper X 0 + 0X >= 0 + 0X proper nil() -> ok nil() 0 >= 1 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 2 + 1X >= 2 + 1X isNePal mark X -> mark isNePal X 1 + 0X >= 0 + 0X U11 ok X -> ok U11 X 1 + 1X >= 1 + 1X U11 mark X -> mark U11 X 0 + 0X >= 0 + 0X U12 ok X -> ok U12 X 1 + 1X >= 1 + 1X U12 mark X -> mark U12 X 0 + 0X >= 0 + 0X active isNePal __(I, __(P, I)) -> mark U11 tt() 0 + 0I + 0P >= 0 active isNePal X -> isNePal active X 0 + 0X >= 1 + 0X active U11 tt() -> mark U12 tt() 0 >= 0 active U11 X -> U11 active X 0 + 0X >= 0 + 0X active U12 tt() -> mark tt() 0 >= 0 active U12 X -> U12 active X 0 + 0X >= 0 + 0X active __(nil(), X) -> mark X 0 + 0X >= 0 + 0X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z active __(X1, X2) -> __(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2 active __(X1, X2) -> __(X1, active X2) 0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2 active __(X, nil()) -> mark X 0 + 0X >= 0 + 0X __(ok X1, ok X2) -> ok __(X1, X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 __(mark X1, X2) -> mark __(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 __(X1, mark X2) -> mark __(X1, X2) 0 + 1X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2, proper# U12 X -> proper# X, proper# U11 X -> proper# X} SCC (4): Strict: {proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2, proper# U12 X -> proper# X, proper# U11 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = x0 + x1, [mark](x0) = 0, [active](x0) = 0, [U12](x0) = x0, [U11](x0) = x0 + 1, [isNePal](x0) = 0, [proper](x0) = 0, [ok](x0) = x0 + 1, [top](x0) = 0, [nil] = 0, [tt] = 0, [proper#](x0) = x0 Strict: proper# U11 X -> proper# X 1 + 1X >= 0 + 1X proper# U12 X -> proper# X 0 + 1X >= 0 + 1X proper# __(X1, X2) -> proper# X2 0 + 1X1 + 1X2 >= 0 + 1X2 proper# __(X1, X2) -> proper# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 0 + 0X proper U11 X -> U11 proper X 0 + 0X >= 1 + 0X proper tt() -> ok tt() 0 >= 1 proper U12 X -> U12 proper X 0 + 0X >= 0 + 0X proper nil() -> ok nil() 0 >= 1 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 0 + 0X >= 1 + 0X isNePal mark X -> mark isNePal X 0 + 0X >= 0 + 0X U11 ok X -> ok U11 X 2 + 1X >= 2 + 1X U11 mark X -> mark U11 X 1 + 0X >= 0 + 0X U12 ok X -> ok U12 X 1 + 1X >= 1 + 1X U12 mark X -> mark U12 X 0 + 0X >= 0 + 0X active isNePal __(I, __(P, I)) -> mark U11 tt() 0 + 0I + 0P >= 0 active isNePal X -> isNePal active X 0 + 0X >= 0 + 0X active U11 tt() -> mark U12 tt() 0 >= 0 active U11 X -> U11 active X 0 + 0X >= 1 + 0X active U12 tt() -> mark tt() 0 >= 0 active U12 X -> U12 active X 0 + 0X >= 0 + 0X active __(nil(), X) -> mark X 0 + 0X >= 0 + 0X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z active __(X1, X2) -> __(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2 active __(X1, X2) -> __(X1, active X2) 0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2 active __(X, nil()) -> mark X 0 + 0X >= 0 + 0X __(ok X1, ok X2) -> ok __(X1, X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 __(mark X1, X2) -> mark __(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 __(X1, mark X2) -> mark __(X1, X2) 0 + 1X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2, proper# U12 X -> proper# X} SCC (3): Strict: {proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2, proper# U12 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = x0 + x1, [mark](x0) = 0, [active](x0) = 0, [U12](x0) = x0 + 1, [U11](x0) = 0, [isNePal](x0) = 1, [proper](x0) = 0, [ok](x0) = x0, [top](x0) = 0, [nil] = 0, [tt] = 1, [proper#](x0) = x0 Strict: proper# U12 X -> proper# X 1 + 1X >= 0 + 1X proper# __(X1, X2) -> proper# X2 0 + 1X1 + 1X2 >= 0 + 1X2 proper# __(X1, X2) -> proper# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 1 + 0X proper U11 X -> U11 proper X 0 + 0X >= 0 + 0X proper tt() -> ok tt() 0 >= 1 proper U12 X -> U12 proper X 0 + 0X >= 1 + 0X proper nil() -> ok nil() 0 >= 0 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 1 + 0X >= 1 + 0X isNePal mark X -> mark isNePal X 1 + 0X >= 0 + 0X U11 ok X -> ok U11 X 0 + 0X >= 0 + 0X U11 mark X -> mark U11 X 0 + 0X >= 0 + 0X U12 ok X -> ok U12 X 1 + 1X >= 1 + 1X U12 mark X -> mark U12 X 1 + 0X >= 0 + 0X active isNePal __(I, __(P, I)) -> mark U11 tt() 0 + 0I + 0P >= 0 active isNePal X -> isNePal active X 0 + 0X >= 1 + 0X active U11 tt() -> mark U12 tt() 0 >= 0 active U11 X -> U11 active X 0 + 0X >= 0 + 0X active U12 tt() -> mark tt() 0 >= 0 active U12 X -> U12 active X 0 + 0X >= 1 + 0X active __(nil(), X) -> mark X 0 + 0X >= 0 + 0X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z active __(X1, X2) -> __(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2 active __(X1, X2) -> __(X1, active X2) 0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2 active __(X, nil()) -> mark X 0 + 0X >= 0 + 0X __(ok X1, ok X2) -> ok __(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 __(mark X1, X2) -> mark __(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 __(X1, mark X2) -> mark __(X1, X2) 0 + 1X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2} SCC (2): Strict: {proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = x0 + x1 + 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [U12](x0) = x0 + 1, [U11](x0) = 0, [isNePal](x0) = x0 + 1, [proper](x0) = 0, [ok](x0) = 0, [top](x0) = 0, [nil] = 0, [tt] = 0, [proper#](x0) = x0 + 1 Strict: proper# __(X1, X2) -> proper# X2 2 + 1X1 + 1X2 >= 1 + 1X2 proper# __(X1, X2) -> proper# X1 2 + 1X1 + 1X2 >= 1 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 1 + 0X proper U11 X -> U11 proper X 0 + 0X >= 0 + 0X proper tt() -> ok tt() 0 >= 0 proper U12 X -> U12 proper X 0 + 0X >= 1 + 0X proper nil() -> ok nil() 0 >= 0 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 1 + 0X >= 0 + 0X isNePal mark X -> mark isNePal X 2 + 1X >= 2 + 1X U11 ok X -> ok U11 X 0 + 0X >= 0 + 0X U11 mark X -> mark U11 X 0 + 0X >= 1 + 0X U12 ok X -> ok U12 X 1 + 0X >= 0 + 0X U12 mark X -> mark U12 X 2 + 1X >= 2 + 1X active isNePal __(I, __(P, I)) -> mark U11 tt() 4 + 2I + 1P >= 1 active isNePal X -> isNePal active X 2 + 1X >= 2 + 1X active U11 tt() -> mark U12 tt() 1 >= 2 active U11 X -> U11 active X 1 + 0X >= 0 + 0X active U12 tt() -> mark tt() 2 >= 1 active U12 X -> U12 active X 2 + 1X >= 2 + 1X active __(nil(), X) -> mark X 2 + 1X >= 1 + 1X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 3 + 1X + 1Y + 1Z >= 3 + 1X + 1Y + 1Z active __(X1, X2) -> __(active X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 active __(X1, X2) -> __(X1, active X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 active __(X, nil()) -> mark X 2 + 1X >= 1 + 1X __(ok X1, ok X2) -> ok __(X1, X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 __(mark X1, X2) -> mark __(X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 __(X1, mark X2) -> mark __(X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 Qed SCC (5): Strict: {active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2, active# U12 X -> active# X, active# U11 X -> active# X, active# isNePal X -> 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = x0 + x1, [mark](x0) = 0, [active](x0) = 0, [U12](x0) = x0, [U11](x0) = x0, [isNePal](x0) = x0 + 1, [proper](x0) = 0, [ok](x0) = x0 + 1, [top](x0) = 0, [nil] = 0, [tt] = 0, [active#](x0) = x0 Strict: active# isNePal X -> active# X 1 + 1X >= 0 + 1X active# U11 X -> active# X 0 + 1X >= 0 + 1X active# U12 X -> active# X 0 + 1X >= 0 + 1X active# __(X1, X2) -> active# X2 0 + 1X1 + 1X2 >= 0 + 1X2 active# __(X1, X2) -> active# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 1 + 0X proper U11 X -> U11 proper X 0 + 0X >= 0 + 0X proper tt() -> ok tt() 0 >= 1 proper U12 X -> U12 proper X 0 + 0X >= 0 + 0X proper nil() -> ok nil() 0 >= 1 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 2 + 1X >= 2 + 1X isNePal mark X -> mark isNePal X 1 + 0X >= 0 + 0X U11 ok X -> ok U11 X 1 + 1X >= 1 + 1X U11 mark X -> mark U11 X 0 + 0X >= 0 + 0X U12 ok X -> ok U12 X 1 + 1X >= 1 + 1X U12 mark X -> mark U12 X 0 + 0X >= 0 + 0X active isNePal __(I, __(P, I)) -> mark U11 tt() 0 + 0I + 0P >= 0 active isNePal X -> isNePal active X 0 + 0X >= 1 + 0X active U11 tt() -> mark U12 tt() 0 >= 0 active U11 X -> U11 active X 0 + 0X >= 0 + 0X active U12 tt() -> mark tt() 0 >= 0 active U12 X -> U12 active X 0 + 0X >= 0 + 0X active __(nil(), X) -> mark X 0 + 0X >= 0 + 0X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z active __(X1, X2) -> __(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2 active __(X1, X2) -> __(X1, active X2) 0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2 active __(X, nil()) -> mark X 0 + 0X >= 0 + 0X __(ok X1, ok X2) -> ok __(X1, X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 __(mark X1, X2) -> mark __(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 __(X1, mark X2) -> mark __(X1, X2) 0 + 1X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2, active# U12 X -> active# X, active# U11 X -> active# X} SCC (4): Strict: {active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2, active# U12 X -> active# X, active# U11 X -> 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = x0 + x1, [mark](x0) = 0, [active](x0) = 0, [U12](x0) = x0, [U11](x0) = x0 + 1, [isNePal](x0) = 0, [proper](x0) = 0, [ok](x0) = x0 + 1, [top](x0) = 0, [nil] = 0, [tt] = 0, [active#](x0) = x0 Strict: active# U11 X -> active# X 1 + 1X >= 0 + 1X active# U12 X -> active# X 0 + 1X >= 0 + 1X active# __(X1, X2) -> active# X2 0 + 1X1 + 1X2 >= 0 + 1X2 active# __(X1, X2) -> active# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 0 + 0X proper U11 X -> U11 proper X 0 + 0X >= 1 + 0X proper tt() -> ok tt() 0 >= 1 proper U12 X -> U12 proper X 0 + 0X >= 0 + 0X proper nil() -> ok nil() 0 >= 1 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 0 + 0X >= 1 + 0X isNePal mark X -> mark isNePal X 0 + 0X >= 0 + 0X U11 ok X -> ok U11 X 2 + 1X >= 2 + 1X U11 mark X -> mark U11 X 1 + 0X >= 0 + 0X U12 ok X -> ok U12 X 1 + 1X >= 1 + 1X U12 mark X -> mark U12 X 0 + 0X >= 0 + 0X active isNePal __(I, __(P, I)) -> mark U11 tt() 0 + 0I + 0P >= 0 active isNePal X -> isNePal active X 0 + 0X >= 0 + 0X active U11 tt() -> mark U12 tt() 0 >= 0 active U11 X -> U11 active X 0 + 0X >= 1 + 0X active U12 tt() -> mark tt() 0 >= 0 active U12 X -> U12 active X 0 + 0X >= 0 + 0X active __(nil(), X) -> mark X 0 + 0X >= 0 + 0X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z active __(X1, X2) -> __(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2 active __(X1, X2) -> __(X1, active X2) 0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2 active __(X, nil()) -> mark X 0 + 0X >= 0 + 0X __(ok X1, ok X2) -> ok __(X1, X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 __(mark X1, X2) -> mark __(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 __(X1, mark X2) -> mark __(X1, X2) 0 + 1X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2, active# U12 X -> active# X} SCC (3): Strict: {active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2, active# U12 X -> 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = x0 + x1, [mark](x0) = 0, [active](x0) = 0, [U12](x0) = x0 + 1, [U11](x0) = 0, [isNePal](x0) = 1, [proper](x0) = 0, [ok](x0) = x0, [top](x0) = 0, [nil] = 0, [tt] = 1, [active#](x0) = x0 Strict: active# U12 X -> active# X 1 + 1X >= 0 + 1X active# __(X1, X2) -> active# X2 0 + 1X1 + 1X2 >= 0 + 1X2 active# __(X1, X2) -> active# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 1 + 0X proper U11 X -> U11 proper X 0 + 0X >= 0 + 0X proper tt() -> ok tt() 0 >= 1 proper U12 X -> U12 proper X 0 + 0X >= 1 + 0X proper nil() -> ok nil() 0 >= 0 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 1 + 0X >= 1 + 0X isNePal mark X -> mark isNePal X 1 + 0X >= 0 + 0X U11 ok X -> ok U11 X 0 + 0X >= 0 + 0X U11 mark X -> mark U11 X 0 + 0X >= 0 + 0X U12 ok X -> ok U12 X 1 + 1X >= 1 + 1X U12 mark X -> mark U12 X 1 + 0X >= 0 + 0X active isNePal __(I, __(P, I)) -> mark U11 tt() 0 + 0I + 0P >= 0 active isNePal X -> isNePal active X 0 + 0X >= 1 + 0X active U11 tt() -> mark U12 tt() 0 >= 0 active U11 X -> U11 active X 0 + 0X >= 0 + 0X active U12 tt() -> mark tt() 0 >= 0 active U12 X -> U12 active X 0 + 0X >= 1 + 0X active __(nil(), X) -> mark X 0 + 0X >= 0 + 0X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z active __(X1, X2) -> __(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2 active __(X1, X2) -> __(X1, active X2) 0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2 active __(X, nil()) -> mark X 0 + 0X >= 0 + 0X __(ok X1, ok X2) -> ok __(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 __(mark X1, X2) -> mark __(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 __(X1, mark X2) -> mark __(X1, X2) 0 + 1X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2} SCC (2): Strict: {active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = x0 + x1 + 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [U12](x0) = x0 + 1, [U11](x0) = 0, [isNePal](x0) = x0 + 1, [proper](x0) = 0, [ok](x0) = 0, [top](x0) = 0, [nil] = 0, [tt] = 0, [active#](x0) = x0 + 1 Strict: active# __(X1, X2) -> active# X2 2 + 1X1 + 1X2 >= 1 + 1X2 active# __(X1, X2) -> active# X1 2 + 1X1 + 1X2 >= 1 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 1 + 0X proper U11 X -> U11 proper X 0 + 0X >= 0 + 0X proper tt() -> ok tt() 0 >= 0 proper U12 X -> U12 proper X 0 + 0X >= 1 + 0X proper nil() -> ok nil() 0 >= 0 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 1 + 0X >= 0 + 0X isNePal mark X -> mark isNePal X 2 + 1X >= 2 + 1X U11 ok X -> ok U11 X 0 + 0X >= 0 + 0X U11 mark X -> mark U11 X 0 + 0X >= 1 + 0X U12 ok X -> ok U12 X 1 + 0X >= 0 + 0X U12 mark X -> mark U12 X 2 + 1X >= 2 + 1X active isNePal __(I, __(P, I)) -> mark U11 tt() 4 + 2I + 1P >= 1 active isNePal X -> isNePal active X 2 + 1X >= 2 + 1X active U11 tt() -> mark U12 tt() 1 >= 2 active U11 X -> U11 active X 1 + 0X >= 0 + 0X active U12 tt() -> mark tt() 2 >= 1 active U12 X -> U12 active X 2 + 1X >= 2 + 1X active __(nil(), X) -> mark X 2 + 1X >= 1 + 1X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 3 + 1X + 1Y + 1Z >= 3 + 1X + 1Y + 1Z active __(X1, X2) -> __(active X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 active __(X1, X2) -> __(X1, active X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 active __(X, nil()) -> mark X 2 + 1X >= 1 + 1X __(ok X1, ok X2) -> ok __(X1, X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 __(mark X1, X2) -> mark __(X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 __(X1, mark X2) -> mark __(X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 Qed SCC (2): Strict: {isNePal# mark X -> isNePal# X, 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = 0, [mark](x0) = x0, [active](x0) = 0, [U12](x0) = 0, [U11](x0) = 0, [isNePal](x0) = 0, [proper](x0) = 0, [ok](x0) = x0 + 1, [top](x0) = 0, [nil] = 1, [tt] = 0, [isNePal#](x0) = x0 Strict: isNePal# ok X -> isNePal# X 1 + 1X >= 0 + 1X isNePal# mark X -> isNePal# X 0 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 0 + 0X proper U11 X -> U11 proper X 0 + 0X >= 0 + 0X proper tt() -> ok tt() 0 >= 1 proper U12 X -> U12 proper X 0 + 0X >= 0 + 0X proper nil() -> ok nil() 0 >= 2 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 0 + 0X >= 1 + 0X isNePal mark X -> mark isNePal X 0 + 0X >= 0 + 0X U11 ok X -> ok U11 X 0 + 0X >= 1 + 0X U11 mark X -> mark U11 X 0 + 0X >= 0 + 0X U12 ok X -> ok U12 X 0 + 0X >= 1 + 0X U12 mark X -> mark U12 X 0 + 0X >= 0 + 0X active isNePal __(I, __(P, I)) -> mark U11 tt() 0 + 0I + 0P >= 0 active isNePal X -> isNePal active X 0 + 0X >= 0 + 0X active U11 tt() -> mark U12 tt() 0 >= 0 active U11 X -> U11 active X 0 + 0X >= 0 + 0X active U12 tt() -> mark tt() 0 >= 0 active U12 X -> U12 active X 0 + 0X >= 0 + 0X active __(nil(), X) -> mark X 0 + 0X >= 0 + 1X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z active __(X1, X2) -> __(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 active __(X1, X2) -> __(X1, active X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 active __(X, nil()) -> mark X 0 + 0X >= 0 + 1X __(ok X1, ok X2) -> ok __(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 __(mark X1, X2) -> mark __(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 __(X1, mark X2) -> mark __(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {isNePal# mark X -> isNePal# X} SCC (1): Strict: {isNePal# mark 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = x0 + x1 + 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [U12](x0) = x0 + 1, [U11](x0) = x0 + 1, [isNePal](x0) = 0, [proper](x0) = 0, [ok](x0) = 0, [top](x0) = 0, [nil] = 0, [tt] = 0, [isNePal#](x0) = x0 Strict: isNePal# mark X -> isNePal# X 1 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 0 + 0X proper U11 X -> U11 proper X 0 + 0X >= 1 + 0X proper tt() -> ok tt() 0 >= 0 proper U12 X -> U12 proper X 0 + 0X >= 1 + 0X proper nil() -> ok nil() 0 >= 0 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 0 + 0X >= 0 + 0X isNePal mark X -> mark isNePal X 0 + 0X >= 1 + 0X U11 ok X -> ok U11 X 1 + 0X >= 0 + 0X U11 mark X -> mark U11 X 2 + 1X >= 2 + 1X U12 ok X -> ok U12 X 1 + 0X >= 0 + 0X U12 mark X -> mark U12 X 2 + 1X >= 2 + 1X active isNePal __(I, __(P, I)) -> mark U11 tt() 1 + 0I + 0P >= 2 active isNePal X -> isNePal active X 1 + 0X >= 0 + 0X active U11 tt() -> mark U12 tt() 2 >= 2 active U11 X -> U11 active X 2 + 1X >= 2 + 1X active U12 tt() -> mark tt() 2 >= 1 active U12 X -> U12 active X 2 + 1X >= 2 + 1X active __(nil(), X) -> mark X 2 + 1X >= 1 + 1X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 3 + 1X + 1Y + 1Z >= 3 + 1X + 1Y + 1Z active __(X1, X2) -> __(active X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 active __(X1, X2) -> __(X1, active X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 active __(X, nil()) -> mark X 2 + 1X >= 1 + 1X __(ok X1, ok X2) -> ok __(X1, X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 __(mark X1, X2) -> mark __(X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 __(X1, mark X2) -> mark __(X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 Qed SCC (2): Strict: {U11# mark X -> U11# X, U11# ok X -> U11# 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = 0, [mark](x0) = x0, [active](x0) = 0, [U12](x0) = 0, [U11](x0) = 0, [isNePal](x0) = 0, [proper](x0) = 0, [ok](x0) = x0 + 1, [top](x0) = 0, [nil] = 1, [tt] = 0, [U11#](x0) = x0 Strict: U11# ok X -> U11# X 1 + 1X >= 0 + 1X U11# mark X -> U11# X 0 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 0 + 0X proper U11 X -> U11 proper X 0 + 0X >= 0 + 0X proper tt() -> ok tt() 0 >= 1 proper U12 X -> U12 proper X 0 + 0X >= 0 + 0X proper nil() -> ok nil() 0 >= 2 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 0 + 0X >= 1 + 0X isNePal mark X -> mark isNePal X 0 + 0X >= 0 + 0X U11 ok X -> ok U11 X 0 + 0X >= 1 + 0X U11 mark X -> mark U11 X 0 + 0X >= 0 + 0X U12 ok X -> ok U12 X 0 + 0X >= 1 + 0X U12 mark X -> mark U12 X 0 + 0X >= 0 + 0X active isNePal __(I, __(P, I)) -> mark U11 tt() 0 + 0I + 0P >= 0 active isNePal X -> isNePal active X 0 + 0X >= 0 + 0X active U11 tt() -> mark U12 tt() 0 >= 0 active U11 X -> U11 active X 0 + 0X >= 0 + 0X active U12 tt() -> mark tt() 0 >= 0 active U12 X -> U12 active X 0 + 0X >= 0 + 0X active __(nil(), X) -> mark X 0 + 0X >= 0 + 1X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z active __(X1, X2) -> __(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 active __(X1, X2) -> __(X1, active X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 active __(X, nil()) -> mark X 0 + 0X >= 0 + 1X __(ok X1, ok X2) -> ok __(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 __(mark X1, X2) -> mark __(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 __(X1, mark X2) -> mark __(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {U11# mark X -> U11# X} SCC (1): Strict: {U11# mark X -> U11# 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = x0 + x1 + 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [U12](x0) = x0 + 1, [U11](x0) = x0 + 1, [isNePal](x0) = 0, [proper](x0) = 0, [ok](x0) = 0, [top](x0) = 0, [nil] = 0, [tt] = 0, [U11#](x0) = x0 Strict: U11# mark X -> U11# X 1 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 0 + 0X proper U11 X -> U11 proper X 0 + 0X >= 1 + 0X proper tt() -> ok tt() 0 >= 0 proper U12 X -> U12 proper X 0 + 0X >= 1 + 0X proper nil() -> ok nil() 0 >= 0 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 0 + 0X >= 0 + 0X isNePal mark X -> mark isNePal X 0 + 0X >= 1 + 0X U11 ok X -> ok U11 X 1 + 0X >= 0 + 0X U11 mark X -> mark U11 X 2 + 1X >= 2 + 1X U12 ok X -> ok U12 X 1 + 0X >= 0 + 0X U12 mark X -> mark U12 X 2 + 1X >= 2 + 1X active isNePal __(I, __(P, I)) -> mark U11 tt() 1 + 0I + 0P >= 2 active isNePal X -> isNePal active X 1 + 0X >= 0 + 0X active U11 tt() -> mark U12 tt() 2 >= 2 active U11 X -> U11 active X 2 + 1X >= 2 + 1X active U12 tt() -> mark tt() 2 >= 1 active U12 X -> U12 active X 2 + 1X >= 2 + 1X active __(nil(), X) -> mark X 2 + 1X >= 1 + 1X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 3 + 1X + 1Y + 1Z >= 3 + 1X + 1Y + 1Z active __(X1, X2) -> __(active X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 active __(X1, X2) -> __(X1, active X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 active __(X, nil()) -> mark X 2 + 1X >= 1 + 1X __(ok X1, ok X2) -> ok __(X1, X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 __(mark X1, X2) -> mark __(X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 __(X1, mark X2) -> mark __(X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 Qed SCC (2): Strict: {U12# mark X -> U12# X, U12# ok X -> U12# 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = 0, [mark](x0) = x0, [active](x0) = 0, [U12](x0) = 0, [U11](x0) = 0, [isNePal](x0) = 0, [proper](x0) = 0, [ok](x0) = x0 + 1, [top](x0) = 0, [nil] = 1, [tt] = 0, [U12#](x0) = x0 Strict: U12# ok X -> U12# X 1 + 1X >= 0 + 1X U12# mark X -> U12# X 0 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 0 + 0X proper U11 X -> U11 proper X 0 + 0X >= 0 + 0X proper tt() -> ok tt() 0 >= 1 proper U12 X -> U12 proper X 0 + 0X >= 0 + 0X proper nil() -> ok nil() 0 >= 2 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 0 + 0X >= 1 + 0X isNePal mark X -> mark isNePal X 0 + 0X >= 0 + 0X U11 ok X -> ok U11 X 0 + 0X >= 1 + 0X U11 mark X -> mark U11 X 0 + 0X >= 0 + 0X U12 ok X -> ok U12 X 0 + 0X >= 1 + 0X U12 mark X -> mark U12 X 0 + 0X >= 0 + 0X active isNePal __(I, __(P, I)) -> mark U11 tt() 0 + 0I + 0P >= 0 active isNePal X -> isNePal active X 0 + 0X >= 0 + 0X active U11 tt() -> mark U12 tt() 0 >= 0 active U11 X -> U11 active X 0 + 0X >= 0 + 0X active U12 tt() -> mark tt() 0 >= 0 active U12 X -> U12 active X 0 + 0X >= 0 + 0X active __(nil(), X) -> mark X 0 + 0X >= 0 + 1X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z active __(X1, X2) -> __(active X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 active __(X1, X2) -> __(X1, active X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 active __(X, nil()) -> mark X 0 + 0X >= 0 + 1X __(ok X1, ok X2) -> ok __(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 __(mark X1, X2) -> mark __(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 __(X1, mark X2) -> mark __(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: {U12# mark X -> U12# X} SCC (1): Strict: {U12# mark X -> U12# 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = x0 + x1 + 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [U12](x0) = x0 + 1, [U11](x0) = x0 + 1, [isNePal](x0) = 0, [proper](x0) = 0, [ok](x0) = 0, [top](x0) = 0, [nil] = 0, [tt] = 0, [U12#](x0) = x0 Strict: U12# mark X -> U12# X 1 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 0 + 0X proper U11 X -> U11 proper X 0 + 0X >= 1 + 0X proper tt() -> ok tt() 0 >= 0 proper U12 X -> U12 proper X 0 + 0X >= 1 + 0X proper nil() -> ok nil() 0 >= 0 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 0 + 0X >= 0 + 0X isNePal mark X -> mark isNePal X 0 + 0X >= 1 + 0X U11 ok X -> ok U11 X 1 + 0X >= 0 + 0X U11 mark X -> mark U11 X 2 + 1X >= 2 + 1X U12 ok X -> ok U12 X 1 + 0X >= 0 + 0X U12 mark X -> mark U12 X 2 + 1X >= 2 + 1X active isNePal __(I, __(P, I)) -> mark U11 tt() 1 + 0I + 0P >= 2 active isNePal X -> isNePal active X 1 + 0X >= 0 + 0X active U11 tt() -> mark U12 tt() 2 >= 2 active U11 X -> U11 active X 2 + 1X >= 2 + 1X active U12 tt() -> mark tt() 2 >= 1 active U12 X -> U12 active X 2 + 1X >= 2 + 1X active __(nil(), X) -> mark X 2 + 1X >= 1 + 1X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 3 + 1X + 1Y + 1Z >= 3 + 1X + 1Y + 1Z active __(X1, X2) -> __(active X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 active __(X1, X2) -> __(X1, active X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 active __(X, nil()) -> mark X 2 + 1X >= 1 + 1X __(ok X1, ok X2) -> ok __(X1, X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 __(mark X1, X2) -> mark __(X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 __(X1, mark X2) -> mark __(X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 Qed SCC (3): 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [active](x0) = 0, [U12](x0) = 0, [U11](x0) = 0, [isNePal](x0) = x0 + 1, [proper](x0) = 0, [ok](x0) = x0 + 1, [top](x0) = 0, [nil] = 1, [tt] = 1, [__#](x0, x1) = x0 + 1 Strict: __#(ok X1, ok X2) -> __#(X1, X2) 2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2 __#(mark X1, X2) -> __#(X1, X2) 2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2 __#(X1, mark X2) -> __#(X1, X2) 1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 1 + 0X proper U11 X -> U11 proper X 0 + 0X >= 0 + 0X proper tt() -> ok tt() 0 >= 2 proper U12 X -> U12 proper X 0 + 0X >= 0 + 0X proper nil() -> ok nil() 0 >= 2 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 2 + 1X >= 2 + 1X isNePal mark X -> mark isNePal X 2 + 1X >= 2 + 1X U11 ok X -> ok U11 X 0 + 0X >= 1 + 0X U11 mark X -> mark U11 X 0 + 0X >= 1 + 0X U12 ok X -> ok U12 X 0 + 0X >= 1 + 0X U12 mark X -> mark U12 X 0 + 0X >= 1 + 0X active isNePal __(I, __(P, I)) -> mark U11 tt() 0 + 0I + 0P >= 1 active isNePal X -> isNePal active X 0 + 0X >= 1 + 0X active U11 tt() -> mark U12 tt() 0 >= 1 active U11 X -> U11 active X 0 + 0X >= 0 + 0X active U12 tt() -> mark tt() 0 >= 2 active U12 X -> U12 active X 0 + 0X >= 0 + 0X active __(nil(), X) -> mark X 0 + 0X >= 1 + 1X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 0 + 0X + 0Y + 0Z >= 3 + 0X + 0Y + 1Z active __(X1, X2) -> __(active X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 active __(X1, X2) -> __(X1, active X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 active __(X, nil()) -> mark X 0 + 0X >= 1 + 1X __(ok X1, ok X2) -> ok __(X1, X2) 2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2 __(mark X1, X2) -> mark __(X1, X2) 1 + 0X1 + 1X2 >= 2 + 0X1 + 1X2 __(X1, mark X2) -> mark __(X1, X2) 2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2 SCCS (1): Scc: {__#(X1, mark X2) -> __#(X1, X2)} SCC (1): 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 U12 X -> U12 active X, active U12 tt() -> mark tt(), active U11 X -> U11 active X, active U11 tt() -> mark U12 tt(), active isNePal X -> isNePal active X, active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> mark U12 X, U12 ok X -> ok U12 X, U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, isNePal mark X -> mark isNePal X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper U12 X -> U12 proper X, proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper isNePal X -> isNePal proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [__](x0, x1) = x0 + x1 + 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [U12](x0) = x0 + 1, [U11](x0) = x0 + 1, [isNePal](x0) = 0, [proper](x0) = 0, [ok](x0) = 0, [top](x0) = 0, [nil] = 0, [tt] = 0, [__#](x0, x1) = x0 Strict: __#(X1, mark X2) -> __#(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper isNePal X -> isNePal proper X 0 + 0X >= 0 + 0X proper U11 X -> U11 proper X 0 + 0X >= 1 + 0X proper tt() -> ok tt() 0 >= 0 proper U12 X -> U12 proper X 0 + 0X >= 1 + 0X proper nil() -> ok nil() 0 >= 0 proper __(X1, X2) -> __(proper X1, proper X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 isNePal ok X -> ok isNePal X 0 + 0X >= 0 + 0X isNePal mark X -> mark isNePal X 0 + 0X >= 1 + 0X U11 ok X -> ok U11 X 1 + 0X >= 0 + 0X U11 mark X -> mark U11 X 2 + 1X >= 2 + 1X U12 ok X -> ok U12 X 1 + 0X >= 0 + 0X U12 mark X -> mark U12 X 2 + 1X >= 2 + 1X active isNePal __(I, __(P, I)) -> mark U11 tt() 1 + 0I + 0P >= 2 active isNePal X -> isNePal active X 1 + 0X >= 0 + 0X active U11 tt() -> mark U12 tt() 2 >= 2 active U11 X -> U11 active X 2 + 1X >= 2 + 1X active U12 tt() -> mark tt() 2 >= 1 active U12 X -> U12 active X 2 + 1X >= 2 + 1X active __(nil(), X) -> mark X 2 + 1X >= 1 + 1X active __(__(X, Y), Z) -> mark __(X, __(Y, Z)) 3 + 1X + 1Y + 1Z >= 3 + 1X + 1Y + 1Z active __(X1, X2) -> __(active X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 active __(X1, X2) -> __(X1, active X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 active __(X, nil()) -> mark X 2 + 1X >= 1 + 1X __(ok X1, ok X2) -> ok __(X1, X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 __(mark X1, X2) -> mark __(X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 __(X1, mark X2) -> mark __(X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 Qed