Further, let \(B_x\)  be the unary NFA with \(m_x\)  states obtained by re-labelling all transitions in \(A_x\)  with a single letter \(a\) . It is clear that the paths of \(A_x\)  correspond bijectively to the paths of \(B_x\) . Further, we compute the NFA \(B^{\prime }_x\) , the Chrobak normal form of the unary automata \(B_x\)  (see [1]}, [2]}).
As such, \(B^{\prime }_x\)  consists of a path of length \(O(m_x^2)\)  ending in a state \(q\) , followed by a single nondeterministic choice from \(q\)  to a set of disjoint cycles of lengths \(c_1, c_2, \ldots , c_h\) , with \(c_i \le m_x\)  for all \(i\le h\) . It follows that there exists a finite set of arithmetic progressions which describe exactly the length of accepted words for \(B^{\prime }_x\) . Let \(\ell ^x_{p,i} + \ell ^x_{c,i}\operatorname{\mathbb {N}}\) , for \(i\in \lbrace 1,\ldots ,d_x\rbrace \) , be these progressions corresponding to \(B^{\prime }_x\) . Note that for each of these lengths (and, accordingly, for each of the accepting paths of \(B^{\prime }_x\) ), there exists a word of corresponding length accepted by \(B_x\) , so there also exists a word of this length in \(R_x\) , and, ultimately, a word of this length in \(L_x\) .
