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())) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(U11(X)) -> U11(active(X)) active(U12(X)) -> U12(active(X)) active(isNePal(X)) -> isNePal(active(X)) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) U11(mark(X)) -> mark(U11(X)) U12(mark(X)) -> mark(U12(X)) isNePal(mark(X)) -> mark(isNePal(X)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(U11(X)) -> U11(proper(X)) proper(tt()) -> ok(tt()) proper(U12(X)) -> U12(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) U11(ok(X)) -> ok(U11(X)) U12(ok(X)) -> ok(U12(X)) isNePal(ok(X)) -> ok(isNePal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Proof: Bounds Processor: bound: 2 enrichment: match automaton: final states: {43,42,41,40,39,19,18,11,10,9,8,7,6,5} transitions: mark0(45) -> 1* mark0(20) -> 1* mark0(2) -> 1* mark0(44) -> 1* mark0(19) -> 1* mark0(4) -> 1* mark0(1) -> 1* mark0(3) -> 1* ok0(20) -> 4* ok0(44) -> 4* ok0(19) -> 4* ok0(4) -> 4* ok0(1) -> 4* ok0(3) -> 4* top0(45) -> 11* top0(20) -> 11* top0(2) -> 11* top0(44) -> 11* top0(19) -> 11* top0(4) -> 11* top0(1) -> 11* top0(3) -> 11* top1(10) -> 11* top1(39) -> 11* top1(19) -> 11* top1(18) -> 11* active1(20) -> 18* active1(44) -> 18* active1(19) -> 18* active1(4) -> 18*,5,10 active1(1) -> 18*,5,10 active1(3) -> 18*,5,10 proper1(45) -> 10* proper1(20) -> 10* proper1(2) -> 10* proper1(44) -> 10* proper1(19) -> 10* proper1(4) -> 10* proper1(1) -> 10* proper1(3) -> 10* ok1(45) -> 19* ok1(40) -> 9* ok1(20) -> 4,19* ok1(42) -> 7* ok1(7) -> 7* ok1(2) -> 19*,4,10 ok1(44) -> 19* ok1(9) -> 9* ok1(41) -> 8* ok1(6) -> 6* ok1(43) -> 6* ok1(8) -> 8* isNePal1(20) -> 9* isNePal1(44) -> 9* isNePal1(19) -> 9* isNePal1(4) -> 9* isNePal1(1) -> 9* isNePal1(3) -> 9* U121(20) -> 8* U121(44) -> 8* U121(19) -> 8* U121(4) -> 8* U121(1) -> 8* U121(3) -> 8* U111(20) -> 7* U111(44) -> 7* U111(19) -> 7* U111(4) -> 7* U111(1) -> 7* U111(3) -> 7* __1(2,20) -> 6* __1(3,1) -> 6* __1(3,3) -> 6* __1(1,45) -> 6* __1(44,2) -> 6* __1(44,4) -> 6* __1(19,2) -> 6* __1(3,19) -> 6* __1(19,4) -> 6* __1(4,2) -> 6* __1(4,4) -> 6* __1(2,44) -> 6* __1(44,20) -> 6* __1(45,1) -> 6* __1(45,3) -> 6* __1(19,20) -> 6* __1(20,1) -> 6* __1(20,3) -> 6* __1(4,20) -> 6* __1(3,45) -> 6* __1(45,19) -> 6* __1(20,19) -> 6* __1(44,44) -> 6* __1(19,44) -> 6* __1(1,2) -> 6* __1(4,44) -> 6* __1(1,4) -> 6* __1(1,20) -> 6* __1(2,1) -> 6* __1(20,45) -> 6* __1(2,3) -> 6* __1(2,19) -> 6* __1(3,2) -> 6* __1(3,4) -> 6* __1(1,44) -> 6* __1(44,1) -> 6* __1(44,3) -> 6* __1(19,1) -> 6* __1(19,3) -> 6* __1(3,20) -> 6* __1(4,1) -> 6* __1(4,3) -> 6* __1(44,19) -> 6* __1(45,4) -> 6* __1(19,19) -> 6* __1(20,2) -> 6* __1(4,19) -> 6* __1(20,4) -> 6* __1(3,44) -> 6* __1(45,20) -> 6* __1(20,20) -> 6* __1(44,45) -> 6* __1(1,1) -> 6* __1(19,45) -> 6* __1(1,3) -> 6* __1(4,45) -> 6* __1(45,44) -> 6* __1(1,19) -> 6* __1(20,44) -> 6* __1(2,4) -> 6* mark1(40) -> 9* mark1(42) -> 7* mark1(7) -> 7* mark1(9) -> 9* mark1(41) -> 8* mark1(6) -> 6* mark1(43) -> 6* mark1(8) -> 8* top2(37) -> 11* top2(39) -> 11* active2(45) -> 37,39* active2(20) -> 18,39*,37 active2(2) -> 18,39*,10,5,37 active2(44) -> 18,37,39* active2(21) -> 37* ok2(45) -> 19*,10 ok2(40) -> 9* ok2(35) -> 8* ok2(42) -> 7* ok2(44) -> 19*,4,10 ok2(41) -> 8* ok2(36) -> 9* ok2(31) -> 6* ok2(21) -> 10* ok2(43) -> 6* ok2(33) -> 7* isNePal2(45) -> 40* isNePal2(20) -> 40*,9,36 isNePal2(2) -> 40*,9,36 isNePal2(44) -> 9,40* U122(45) -> 41* U122(20) -> 41*,8,35 U122(2) -> 41*,8,35 U122(44) -> 8,41* U112(45) -> 42* U112(20) -> 42*,7,33 U112(2) -> 42*,7,33 U112(44) -> 7,42* __2(2,20) -> 43*,6,31 __2(44,2) -> 6,43* __2(2,44) -> 6,43* __2(44,20) -> 6,43* __2(44,44) -> 6,43* __2(45,45) -> 43* __2(20,45) -> 6,43* __2(2,45) -> 43* __2(45,2) -> 43* __2(20,2) -> 43*,6,31 __2(45,20) -> 6,43* __2(20,20) -> 43*,6,31 __2(44,45) -> 6,43* __2(45,44) -> 6,43* __2(20,44) -> 6,43* __2(2,2) -> 43*,6,31 tt2() -> 20,44*,2,3,21 nil2() -> 45*,2,21 problem: Qed