This problem comes from a typing problem (non structural subtype assignment).

Given a regular language R, does there exist a regular language U such that:

- U is an antichain for the prefix ordering
- \(\forall u \in U, \exists r \in R, r < u < r^\omega\)
- \(\exists u \in U, r \in R, r < u < r^\omega \wedge |r^{-1}u| > ||U||\)

where \(||U||\) is the number of states of the minimal automaton recognizing \(U\), and \(r^\omega\) is the infinite iteration of \(r\).

I conjecture that such language does not exist, though I don't find an approach to attack it. If such a language does exist, it would be interesting to know if there can be an infinite number of words such that the third point holds or not.