Problem: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(U11(tt())) -> mark(U12(tt())) active(U12(tt())) -> mark(tt()) active(isNePal(__(I,__(P,I)))) -> mark(U11(tt())) mark(__(X1,X2)) -> active(__(mark(X1),mark(X2))) mark(nil()) -> active(nil()) mark(U11(X)) -> active(U11(mark(X))) mark(tt()) -> active(tt()) mark(U12(X)) -> active(U12(mark(X))) mark(isNePal(X)) -> active(isNePal(mark(X))) __(mark(X1),X2) -> __(X1,X2) __(X1,mark(X2)) -> __(X1,X2) __(active(X1),X2) -> __(X1,X2) __(X1,active(X2)) -> __(X1,X2) U11(mark(X)) -> U11(X) U11(active(X)) -> U11(X) U12(mark(X)) -> U12(X) U12(active(X)) -> U12(X) isNePal(mark(X)) -> isNePal(X) isNePal(active(X)) -> isNePal(X) Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {14,8,7,6,5,4,3} transitions: active0(12) -> 3* active0(2) -> 3* active0(1) -> 3* active0(13) -> 3* __0(2,12) -> 5* __0(13,1) -> 5* __0(13,13) -> 5* __0(1,2) -> 5* __0(1,12) -> 5* __0(12,1) -> 5* __0(2,1) -> 5* __0(12,13) -> 5* __0(2,13) -> 5* __0(13,2) -> 5* __0(13,12) -> 5* __0(1,1) -> 5* __0(1,13) -> 5* __0(12,2) -> 5* __0(2,2) -> 5* __0(12,12) -> 5* mark0(12) -> 4* mark0(2) -> 4* mark0(1) -> 4* mark0(13) -> 4* nil0() -> 1* U110(12) -> 6* U110(2) -> 6* U110(1) -> 6* U110(13) -> 6* tt0() -> 2* U120(12) -> 7* U120(2) -> 7* U120(1) -> 7* U120(13) -> 7* isNePal0(12) -> 8* isNePal0(2) -> 8* isNePal0(1) -> 8* isNePal0(13) -> 8* active1(12) -> 14*,3,4 active1(9) -> 4* active1(13) -> 14*,3,4 tt1() -> 12*,2,9 nil1() -> 13*,1,9 problem: Qed