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