YES(?,O(n^1)) 0.15/0.25 YES(?,O(n^1)) 0.15/0.25 0.15/0.25 Problem: 0.15/0.25 zeros() -> cons(0(),n__zeros()) 0.15/0.25 tail(cons(X,XS)) -> activate(XS) 0.15/0.25 zeros() -> n__zeros() 0.15/0.25 activate(n__zeros()) -> zeros() 0.15/0.25 activate(X) -> X 0.15/0.25 0.15/0.25 Proof: 0.15/0.25 Bounds Processor: 0.15/0.25 bound: 2 0.15/0.25 enrichment: match 0.15/0.25 automaton: 0.15/0.25 final states: {6,5,4} 0.15/0.25 transitions: 0.15/0.25 zeros1() -> 5,6 0.15/0.25 n__zeros1() -> 4,7 0.15/0.25 activate1(2) -> 5* 0.15/0.25 activate1(1) -> 5* 0.15/0.25 activate1(3) -> 5* 0.15/0.25 cons1(8,7) -> 4* 0.15/0.25 01() -> 8* 0.15/0.25 n__zeros2() -> 5,6,13 0.15/0.25 cons2(14,6) -> 5* 0.15/0.25 cons2(14,13) -> 6* 0.15/0.25 zeros0() -> 4* 0.15/0.25 02() -> 14* 0.15/0.25 cons0(3,1) -> 1* 0.15/0.25 cons0(3,3) -> 1* 0.15/0.25 cons0(1,2) -> 1* 0.15/0.25 cons0(2,1) -> 1* 0.15/0.25 cons0(2,3) -> 1* 0.15/0.25 cons0(3,2) -> 1* 0.15/0.25 cons0(1,1) -> 1* 0.15/0.25 cons0(1,3) -> 1* 0.15/0.25 cons0(2,2) -> 1* 0.15/0.25 00() -> 2* 0.15/0.25 n__zeros0() -> 3* 0.15/0.25 tail0(2) -> 5* 0.15/0.25 tail0(1) -> 5* 0.15/0.25 tail0(3) -> 5* 0.15/0.25 activate0(2) -> 6* 0.15/0.25 activate0(1) -> 6* 0.15/0.25 activate0(3) -> 6* 0.15/0.25 1 -> 5,6 0.15/0.25 2 -> 5,6 0.15/0.25 3 -> 5,6 0.15/0.25 problem: 0.15/0.25 0.15/0.25 Qed 0.15/0.26 EOF