Pre*: The Predecessors of a Regular Language w.r.t. a Context-Free Grammar, with Applications. - Tassilo Lemke; Tobias Nipkow (Arch. Formal Proofs, 2025)