YES(?,O(n^1)) 0.16/0.58 YES(?,O(n^1)) 0.16/0.58 0.16/0.58 Problem: 0.16/0.58 active(zeros()) -> mark(cons(0(),zeros())) 0.16/0.58 active(tail(cons(X,XS))) -> mark(XS) 0.16/0.58 active(cons(X1,X2)) -> cons(active(X1),X2) 0.16/0.58 active(tail(X)) -> tail(active(X)) 0.16/0.58 cons(mark(X1),X2) -> mark(cons(X1,X2)) 0.16/0.58 tail(mark(X)) -> mark(tail(X)) 0.16/0.58 proper(zeros()) -> ok(zeros()) 0.16/0.58 proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) 0.16/0.58 proper(0()) -> ok(0()) 0.16/0.58 proper(tail(X)) -> tail(proper(X)) 0.16/0.58 cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) 0.16/0.58 tail(ok(X)) -> ok(tail(X)) 0.16/0.58 top(mark(X)) -> top(proper(X)) 0.16/0.58 top(ok(X)) -> top(active(X)) 0.16/0.58 0.16/0.58 Proof: 0.16/0.58 Bounds Processor: 0.16/0.58 bound: 5 0.16/0.58 enrichment: match 0.16/0.58 automaton: 0.16/0.58 final states: {9,8,7,6,5} 0.16/0.58 transitions: 0.16/0.58 ok3(45) -> 37* 0.16/0.58 ok3(42) -> 36* 0.16/0.58 ok3(41) -> 22* 0.16/0.58 cons3(37,36) -> 35* 0.16/0.58 cons3(28,27) -> 41* 0.16/0.58 active3(41) -> 35* 0.16/0.58 03() -> 45* 0.16/0.58 zeros3() -> 42* 0.16/0.58 ok4(48) -> 35* 0.16/0.58 cons4(47,27) -> 35* 0.16/0.58 cons4(45,42) -> 48* 0.16/0.58 active4(48) -> 51* 0.16/0.58 active4(28) -> 47* 0.16/0.58 top4(51) -> 9* 0.16/0.58 cons5(52,42) -> 51* 0.16/0.58 active0(2) -> 5* 0.16/0.58 active0(4) -> 5* 0.16/0.58 active0(1) -> 5* 0.16/0.58 active0(3) -> 5* 0.16/0.58 active5(45) -> 52* 0.16/0.58 zeros0() -> 1* 0.16/0.58 mark0(2) -> 2* 0.16/0.58 mark0(4) -> 2* 0.16/0.58 mark0(1) -> 2* 0.16/0.58 mark0(3) -> 2* 0.16/0.58 cons0(3,1) -> 6* 0.16/0.58 cons0(3,3) -> 6* 0.16/0.58 cons0(4,2) -> 6* 0.16/0.58 cons0(4,4) -> 6* 0.16/0.58 cons0(1,2) -> 6* 0.16/0.58 cons0(1,4) -> 6* 0.16/0.58 cons0(2,1) -> 6* 0.16/0.58 cons0(2,3) -> 6* 0.16/0.58 cons0(3,2) -> 6* 0.16/0.58 cons0(3,4) -> 6* 0.16/0.58 cons0(4,1) -> 6* 0.16/0.58 cons0(4,3) -> 6* 0.16/0.58 cons0(1,1) -> 6* 0.16/0.58 cons0(1,3) -> 6* 0.16/0.58 cons0(2,2) -> 6* 0.16/0.58 cons0(2,4) -> 6* 0.16/0.58 00() -> 3* 0.16/0.58 tail0(2) -> 7* 0.16/0.58 tail0(4) -> 7* 0.16/0.58 tail0(1) -> 7* 0.16/0.58 tail0(3) -> 7* 0.16/0.58 proper0(2) -> 8* 0.16/0.58 proper0(4) -> 8* 0.16/0.58 proper0(1) -> 8* 0.16/0.58 proper0(3) -> 8* 0.16/0.58 ok0(2) -> 4* 0.16/0.58 ok0(4) -> 4* 0.16/0.58 ok0(1) -> 4* 0.16/0.58 ok0(3) -> 4* 0.16/0.58 top0(2) -> 9* 0.16/0.58 top0(4) -> 9* 0.16/0.58 top0(1) -> 9* 0.16/0.58 top0(3) -> 9* 0.16/0.58 top1(21) -> 9* 0.16/0.58 active1(2) -> 21* 0.16/0.58 active1(4) -> 21* 0.16/0.58 active1(1) -> 21* 0.16/0.58 active1(3) -> 21* 0.16/0.58 proper1(2) -> 21* 0.16/0.58 proper1(4) -> 21* 0.16/0.58 proper1(1) -> 21* 0.16/0.58 proper1(3) -> 21* 0.16/0.58 ok1(10) -> 21,8 0.16/0.58 ok1(17) -> 17,6 0.16/0.58 ok1(19) -> 19,7 0.16/0.58 ok1(11) -> 21,8 0.16/0.58 tail1(2) -> 19* 0.16/0.58 tail1(4) -> 19* 0.16/0.58 tail1(1) -> 19* 0.16/0.58 tail1(3) -> 19* 0.16/0.58 cons1(3,1) -> 17* 0.16/0.58 cons1(3,3) -> 17* 0.16/0.58 cons1(4,2) -> 17* 0.16/0.58 cons1(4,4) -> 17* 0.16/0.58 cons1(1,2) -> 17* 0.16/0.58 cons1(1,4) -> 17* 0.16/0.58 cons1(11,10) -> 12* 0.16/0.58 cons1(2,1) -> 17* 0.16/0.58 cons1(2,3) -> 17* 0.16/0.58 cons1(3,2) -> 17* 0.16/0.58 cons1(3,4) -> 17* 0.16/0.58 cons1(4,1) -> 17* 0.16/0.58 cons1(4,3) -> 17* 0.16/0.58 cons1(1,1) -> 17* 0.16/0.58 cons1(1,3) -> 17* 0.16/0.58 cons1(2,2) -> 17* 0.16/0.58 cons1(2,4) -> 17* 0.16/0.58 01() -> 11* 0.16/0.58 zeros1() -> 10* 0.16/0.58 mark1(17) -> 17,6 0.16/0.58 mark1(12) -> 21,5 0.16/0.58 mark1(19) -> 19,7 0.16/0.58 top2(22) -> 9* 0.16/0.58 active2(10) -> 22* 0.16/0.58 active2(11) -> 22* 0.16/0.58 proper2(10) -> 30* 0.16/0.58 proper2(12) -> 22* 0.16/0.58 proper2(11) -> 31* 0.16/0.58 cons2(28,27) -> 29* 0.16/0.58 cons2(31,30) -> 22* 0.16/0.58 mark2(29) -> 22* 0.16/0.58 02() -> 28* 0.16/0.58 zeros2() -> 27* 0.16/0.58 top3(35) -> 9* 0.16/0.58 proper3(27) -> 36* 0.16/0.58 proper3(29) -> 35* 0.16/0.58 proper3(28) -> 37* 0.16/0.58 ok2(27) -> 30* 0.16/0.58 ok2(28) -> 31* 0.16/0.58 problem: 0.16/0.58 0.16/0.58 Qed 0.16/0.59 EOF