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