Resumen
In this paper, we return to the topic, related to one important binary relation on the set of formal languages (considered primarily on the set of iterations of nonempty finite languages), i.e. the equivalence relation at infinity. First of all, we consider examples of the application of this relation (both examples of the need for its implementation, and examples of its use) in various fields of the theory of formal languages, discrete mathematics, and abstract algebra. To simplify the consideration of equivalence at infinity we formulate a simpler binary relation over the set of languages, i.e. the covering relation, the double application of which is equivalent to the application of the equivalence relation at infinity. Next, we consider an algorithm for verifying the fulfillment of the coverage relation, and then we define auxiliary objects used both for proving the correctness of this algorithm and for other problems in the theory of formal languages. As one of the comments on the algorithm, we give the corresponding computer program, consider examples of its operation for specific input languages, after that, we formulate the definitions of the objects associated with them, in particular, the definition of infinite trees of the coverage relation. With their help we prove the correctness of the algorithm for checking the fulfillment of the coverage relation, and also estimate the complexity of this algorithm.